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

Assume Hhom: homeomorphism X Tx Y Ty f.

An exact proof term for the current goal is (continuous_map_topology_dom X Tx Y Ty f (homeomorphism_continuous X Tx Y Ty f Hhom)).

∎