Let Xi be given.

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

We prove the intermediate claim HX0: product_space Empty Xi = {Empty}.

An exact proof term for the current goal is (product_space_empty_index Xi).

We prove the intermediate claim HT0: topology_on (product_space Empty Xi) (product_topology_full Empty Xi).

An exact proof term for the current goal is (product_topology_full_empty_is_topology Xi).

An exact proof term for the current goal is (compact_space_singleton (product_space Empty Xi) (product_topology_full Empty Xi) Empty HX0 HT0).

∎