Let Xi be given.

We will prove topology_on (product_space Empty Xi) (product_topology_full Empty Xi).

We prove the intermediate claim HcompTop: ∀i : set, i ∈ Empty → topology_on (space_family_set Xi i) (space_family_topology Xi i).

Let i be given.

Assume Hi0: i ∈ Empty.

Apply FalseE to the current goal.

An exact proof term for the current goal is (EmptyE i Hi0 False).

An exact proof term for the current goal is (product_topology_full_is_topology Empty Xi HcompTop).

∎