Let X, Tx, Y, Ty and f be given.
Assume Hhom: homeomorphism X Tx Y Ty f.
We will prove ∃g : set, continuous_map Y Ty X Tx g ∧ (∀x : set, x ∈ X → apply_fun g (apply_fun f x) = x) ∧ (∀y : set, y ∈ Y → apply_fun f (apply_fun g y) = y).
An exact proof term for the current goal is (andER (continuous_map X Tx Y Ty f) (∃g : set, continuous_map Y Ty X Tx g ∧ (∀x : set, x ∈ X → apply_fun g (apply_fun f x) = x) ∧ (∀y : set, y ∈ Y → apply_fun f (apply_fun g y) = y)) Hhom).
∎