let T1, T2 be TopSpace; :: thesis: for f being Function of T1,T2
for g being Function of TopStruct(# the carrier of T1, the topology of T1 #),TopStruct(# the carrier of T2, the topology of T2 #) st g = f & g is being_homeomorphism holds
f is being_homeomorphism
let f be Function of T1,T2; :: thesis: for g being Function of TopStruct(# the carrier of T1, the topology of T1 #),TopStruct(# the carrier of T2, the topology of T2 #) st g = f & g is being_homeomorphism holds
f is being_homeomorphism
let g be Function of TopStruct(# the carrier of T1, the topology of T1 #),TopStruct(# the carrier of T2, the topology of T2 #); :: thesis: ( g = f & g is being_homeomorphism implies f is being_homeomorphism )
assume that
A1: g = f and
A2: g is being_homeomorphism ; :: thesis: f is being_homeomorphism
( dom f = [#] TopStruct(# the carrier of T1, the topology of T1 #) & rng f = [#] TopStruct(# the carrier of T2, the topology of T2 #) ) by A1, A2, TOPS_2:def 5;
hence ( dom f = [#] T1 & rng f = [#] T2 ) ; :: according to TOPS_2:def 5 :: thesis: ( f is one-to-one & f is continuous & f " is continuous )
thus f is one-to-one by A1, A2; :: thesis: ( f is continuous & f " is continuous )
thus f is continuous by A1, A2, PRE_TOPC:34; :: thesis: f " is continuous
g " is continuous by A2, TOPS_2:def 5;
hence f " is continuous by A1, PRE_TOPC:34; :: thesis: verum