Let X, Tx, Y, Ty and f be given.

Assume H: continuous_map_total X Tx Y Ty f.

We will prove continuous_map X Tx Y Ty f.

We will prove ((topology_on X Tx ∧ topology_on Y Ty) ∧ function_on f X Y) ∧ (∀V : set, V ∈ Ty → preimage_of X f V ∈ Tx).

We prove the intermediate claim Hcore: ((topology_on X Tx ∧ topology_on Y Ty) ∧ total_function_on f X Y) ∧ (∀V : set, V ∈ Ty → preimage_of X f V ∈ Tx).

An exact proof term for the current goal is H.

We prove the intermediate claim Hleft: (topology_on X Tx ∧ topology_on Y Ty) ∧ total_function_on f X Y.

An exact proof term for the current goal is (andEL ((topology_on X Tx ∧ topology_on Y Ty) ∧ total_function_on f X Y) (∀V : set, V ∈ Ty → preimage_of X f V ∈ Tx) Hcore).

We prove the intermediate claim Hright: ∀V : set, V ∈ Ty → preimage_of X f V ∈ Tx.

An exact proof term for the current goal is (andER ((topology_on X Tx ∧ topology_on Y Ty) ∧ total_function_on f X Y) (∀V : set, V ∈ Ty → preimage_of X f V ∈ Tx) Hcore).

We prove the intermediate claim Htops: topology_on X Tx ∧ topology_on Y Ty.

An exact proof term for the current goal is (andEL (topology_on X Tx ∧ topology_on Y Ty) (total_function_on f X Y) Hleft).

We prove the intermediate claim Htot: total_function_on f X Y.

An exact proof term for the current goal is (andER (topology_on X Tx ∧ topology_on Y Ty) (total_function_on f X Y) Hleft).

We prove the intermediate claim Hfun: function_on f X Y.

An exact proof term for the current goal is (total_function_on_function_on f X Y Htot).

Apply andI to the current goal.

An exact proof term for the current goal is Htops.

An exact proof term for the current goal is Hfun.

An exact proof term for the current goal is Hright.

∎