Let I, Xi and s be given.
Assume Hs: s ∈ product_subbasis_full I Xi.
We will prove ∃i : set, i ∈ I ∧ ∃U : set, U ∈ space_family_topology Xi i ∧ s = product_cylinder I Xi i U.
Set Fam to be the term (λi : set ⇒ {product_cylinder I Xi i U|U ∈ space_family_topology Xi i}).
We prove the intermediate claim Hexi: ∃i ∈ I, s ∈ Fam i.
An exact proof term for the current goal is (famunionE I Fam s Hs).
Apply Hexi to the current goal.
Let i be given.
Assume Hipack.
We prove the intermediate claim HiI: i ∈ I.
An exact proof term for the current goal is (andEL (i ∈ I) (s ∈ Fam i) Hipack).
We prove the intermediate claim HsFam: s ∈ Fam i.
An exact proof term for the current goal is (andER (i ∈ I) (s ∈ Fam i) Hipack).
We use i to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HiI.
An exact proof term for the current goal is (ReplE (space_family_topology Xi i) (λU0 : set ⇒ product_cylinder I Xi i U0) s HsFam).
∎