Let I and Xi be given.
Assume HcompTop: ∀i : set, i ∈ I → topology_on (space_family_set Xi i) (space_family_topology Xi i).
We will prove topology_on (product_space I Xi) (product_topology_full I Xi).
Apply (xm (I = Empty)) to the current goal.
Assume HI0: I = Empty.
rewrite the current goal using HI0 (from left to right).
We prove the intermediate claim Hdef: product_topology_full Empty Xi = countable_product_topology_subbasis Empty Xi.
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
An exact proof term for the current goal is (countable_product_topology_subbasis_empty_is_topology Xi).
Assume HIne: I ≠ Empty.
We prove the intermediate claim HS: subbasis_on (product_space I Xi) (product_subbasis_full I Xi).
An exact proof term for the current goal is (product_subbasis_full_subbasis_on I Xi HIne HcompTop).
We prove the intermediate claim Hdef: product_topology_full I Xi = generated_topology_from_subbasis (product_space I Xi) (product_subbasis_full I Xi).
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
An exact proof term for the current goal is (topology_from_subbasis_is_topology (product_space I Xi) (product_subbasis_full I Xi) HS).
∎