Let f be given.

We will prove f ∈ {Empty}.

We prove the intermediate claim HfPow: f ∈ 𝒫 (setprod Empty (space_family_union Empty Xi)).

An exact proof term for the current goal is (SepE1 (𝒫 (setprod Empty (space_family_union Empty Xi))) (λf0 : set ⇒ total_function_on f0 Empty (space_family_union Empty Xi) ∧ functional_graph f0 ∧ ∀i : set, i ∈ Empty → apply_fun f0 i ∈ space_family_set Xi i) f Hf).

We prove the intermediate claim Heqprod: setprod Empty (space_family_union Empty Xi) = Empty.

An exact proof term for the current goal is (setprod_Empty_left (space_family_union Empty Xi)).

We prove the intermediate claim HfPowE: f ∈ 𝒫 Empty.

rewrite the current goal using Heqprod (from right to left).

An exact proof term for the current goal is HfPow.

We prove the intermediate claim Hsub: f ⊆ Empty.

An exact proof term for the current goal is (PowerE Empty f HfPowE).

We prove the intermediate claim Hall: ∀x : set, x ∉ f.

Let x be given.

Assume Hx: x ∈ f.

We will prove False.

We prove the intermediate claim HxE: x ∈ Empty.

An exact proof term for the current goal is (Hsub x Hx).

An exact proof term for the current goal is (EmptyE x HxE False).

We prove the intermediate claim HfEq: f = Empty.

An exact proof term for the current goal is (Empty_eq f Hall).

rewrite the current goal using HfEq (from left to right).

An exact proof term for the current goal is (SingI Empty).

Let f be given.

Assume Hf: f ∈ {Empty}.

We will prove f ∈ product_space Empty Xi.

We prove the intermediate claim Hfeq: f = Empty.

An exact proof term for the current goal is (SingE Empty f Hf).

rewrite the current goal using Hfeq (from left to right).

We prove the intermediate claim Hpow: Empty ∈ 𝒫 (setprod Empty (space_family_union Empty Xi)).

We prove the intermediate claim Heqprod: setprod Empty (space_family_union Empty Xi) = Empty.

An exact proof term for the current goal is (setprod_Empty_left (space_family_union Empty Xi)).

rewrite the current goal using Heqprod (from left to right).

An exact proof term for the current goal is (Empty_In_Power Empty).

We prove the intermediate claim Htot: total_function_on Empty Empty (space_family_union Empty Xi).

We prove the intermediate claim Hfun: function_on Empty Empty (space_family_union Empty Xi).

Let x be given.

Assume Hx: x ∈ Empty.

We will prove apply_fun Empty x ∈ space_family_union Empty Xi.

An exact proof term for the current goal is (EmptyE x Hx (apply_fun Empty x ∈ space_family_union Empty Xi)).

We prove the intermediate claim Htot': ∀x : set, x ∈ Empty → ∃y : set, y ∈ space_family_union Empty Xi ∧ (x,y) ∈ Empty.

Let x be given.

Assume Hx: x ∈ Empty.

We will prove ∃y : set, y ∈ space_family_union Empty Xi ∧ (x,y) ∈ Empty.

An exact proof term for the current goal is (EmptyE x Hx (∃y : set, y ∈ space_family_union Empty Xi ∧ (x,y) ∈ Empty)).

An exact proof term for the current goal is (andI (function_on Empty Empty (space_family_union Empty Xi)) (∀x : set, x ∈ Empty → ∃y : set, y ∈ space_family_union Empty Xi ∧ (x,y) ∈ Empty) Hfun Htot').

We prove the intermediate claim Hgraph: functional_graph Empty.

Let x, y1 and y2 be given.

Assume H1: (x,y1) ∈ Empty.

Assume H2: (x,y2) ∈ Empty.

An exact proof term for the current goal is (EmptyE (x,y1) H1 (y1 = y2)).

We prove the intermediate claim Hcoords: ∀i : set, i ∈ Empty → apply_fun Empty i ∈ space_family_set Xi i.

Let i be given.

Assume Hi: i ∈ Empty.

We will prove apply_fun Empty i ∈ space_family_set Xi i.

An exact proof term for the current goal is (EmptyE i Hi (apply_fun Empty i ∈ space_family_set Xi i)).

We prove the intermediate claim Hpred: total_function_on Empty Empty (space_family_union Empty Xi) ∧ functional_graph Empty ∧ ∀i : set, i ∈ Empty → apply_fun Empty i ∈ space_family_set Xi i.

Apply andI to the current goal.

An exact proof term for the current goal is Htot.

An exact proof term for the current goal is Hgraph.

An exact proof term for the current goal is Hcoords.

An exact proof term for the current goal is (SepI (𝒫 (setprod Empty (space_family_union Empty Xi))) (λf0 : set ⇒ total_function_on f0 Empty (space_family_union Empty Xi) ∧ functional_graph f0 ∧ ∀i : set, i ∈ Empty → apply_fun f0 i ∈ space_family_set Xi i) Empty Hpow Hpred).