We will prove (Hausdorff_space (product_space Idx Fam) (product_topology_full Idx Fam) → ∀i : set, i ∈ Idx → ∃Xi Txi : set, apply_fun Fam i = (Xi,Txi) ∧ Hausdorff_space Xi Txi) ∧ (regular_space (product_space Idx Fam) (product_topology_full Idx Fam) → ∀i : set, i ∈ Idx → ∃Xi Txi : set, apply_fun Fam i = (Xi,Txi) ∧ regular_space Xi Txi) ∧ (normal_space (product_space Idx Fam) (product_topology_full Idx Fam) → ∀i : set, i ∈ Idx → ∃Xi Txi : set, apply_fun Fam i = (Xi,Txi) ∧ normal_space Xi Txi).

Apply andI to the current goal.

Assume HHprod: Hausdorff_space (product_space Idx Fam) (product_topology_full Idx Fam).

Let i be given.

Assume Hi: i ∈ Idx.

Apply (Hnonempty i Hi) to the current goal.

Let Xi be given.

Assume HexTxi: ∃Txi : set, apply_fun Fam i = (Xi,Txi) ∧ Xi ≠ Empty.

Apply HexTxi to the current goal.

Let Txi be given.

Assume Hpair: apply_fun Fam i = (Xi,Txi) ∧ Xi ≠ Empty.

We prove the intermediate claim HFi: apply_fun Fam i = (Xi,Txi).

An exact proof term for the current goal is (andEL (apply_fun Fam i = (Xi,Txi)) (Xi ≠ Empty) Hpair).

We use Xi to witness the existential quantifier.

We use Txi to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HFi.

The rest of this subproof is missing.

Assume HRprod: regular_space (product_space Idx Fam) (product_topology_full Idx Fam).

Let i be given.

Assume Hi: i ∈ Idx.

Apply (Hnonempty i Hi) to the current goal.

Let Xi be given.

Assume HexTxi: ∃Txi : set, apply_fun Fam i = (Xi,Txi) ∧ Xi ≠ Empty.

Apply HexTxi to the current goal.

Let Txi be given.

Assume Hpair: apply_fun Fam i = (Xi,Txi) ∧ Xi ≠ Empty.

We prove the intermediate claim HFi: apply_fun Fam i = (Xi,Txi).

An exact proof term for the current goal is (andEL (apply_fun Fam i = (Xi,Txi)) (Xi ≠ Empty) Hpair).

We use Xi to witness the existential quantifier.

We use Txi to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HFi.

The rest of this subproof is missing.

Assume HNprod: normal_space (product_space Idx Fam) (product_topology_full Idx Fam).

Let i be given.

Assume Hi: i ∈ Idx.

Apply (Hnonempty i Hi) to the current goal.

Let Xi be given.

Assume HexTxi: ∃Txi : set, apply_fun Fam i = (Xi,Txi) ∧ Xi ≠ Empty.

Apply HexTxi to the current goal.

Let Txi be given.

Assume Hpair: apply_fun Fam i = (Xi,Txi) ∧ Xi ≠ Empty.

We prove the intermediate claim HFi: apply_fun Fam i = (Xi,Txi).

An exact proof term for the current goal is (andEL (apply_fun Fam i = (Xi,Txi)) (Xi ≠ Empty) Hpair).

We use Xi to witness the existential quantifier.

We use Txi to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HFi.

The rest of this subproof is missing.