Let Xi be given.
We will prove topology_on (product_space Empty Xi) (countable_product_topology_subbasis Empty Xi).
We prove the intermediate claim HTdef: countable_product_topology_subbasis Empty Xi = generated_topology_from_subbasis (product_space Empty Xi) (product_subbasis_full Empty Xi).
Use reflexivity.
rewrite the current goal using HTdef (from left to right).
We prove the intermediate claim HS0: product_subbasis_full Empty Xi = Empty.
An exact proof term for the current goal is (famunion_Empty (λi : set ⇒ {product_cylinder Empty Xi i U|U ∈ space_family_topology Xi i})).
rewrite the current goal using HS0 (from left to right).
We prove the intermediate claim HGTS0: generated_topology_from_subbasis (product_space Empty Xi) Empty = generated_topology (product_space Empty Xi) (basis_of_subbasis (product_space Empty Xi) Empty).
Use reflexivity.
rewrite the current goal using HGTS0 (from left to right).
We prove the intermediate claim HX0ne: product_space Empty Xi ≠ Empty.
Assume HX0E: product_space Empty Xi = Empty.
We prove the intermediate claim Hem: Empty ∈ product_space Empty Xi.
rewrite the current goal using (product_space_empty_index Xi) (from left to right).
An exact proof term for the current goal is (SingI Empty).
We prove the intermediate claim HemE: Empty ∈ Empty.
rewrite the current goal using HX0E (from right to left) at position 2.
An exact proof term for the current goal is Hem.
An exact proof term for the current goal is (EmptyE Empty HemE False).
We prove the intermediate claim HB0eq: basis_of_subbasis (product_space Empty Xi) Empty = {product_space Empty Xi}.
An exact proof term for the current goal is (basis_of_subbasis_empty_eq (product_space Empty Xi) HX0ne).
We prove the intermediate claim HB0: basis_on (product_space Empty Xi) (basis_of_subbasis (product_space Empty Xi) Empty).
rewrite the current goal using HB0eq (from left to right).
An exact proof term for the current goal is (basis_on_singleton (product_space Empty Xi)).
An exact proof term for the current goal is (lemma_topology_from_basis (product_space Empty Xi) (basis_of_subbasis (product_space Empty Xi) Empty) HB0).
∎