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

Assume H: continuous_map_total X Tx Y Ty f.

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) H).

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).

∎