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 Z: ( g = f & g is being_homeomorphism ) ; :: thesis: f is being_homeomorphism
then ( dom f = [#] TopStruct(# the carrier of T1,the topology of T1 #) & rng f = [#] TopStruct(# the carrier of T2,the topology of T2 #) ) by Z, TOPS_2:def 5;
hence ( dom f = [#] T1 & rng f = [#] T2 ) by Z, TOPS_2:def 5; :: according to TOPS_2:def 5 :: thesis: ( f is one-to-one & f is continuous & f /" is continuous )
hence f is one-to-one by Z, TOPS_2:def 5; :: thesis: ( f is continuous & f /" is continuous )
thus f is continuous by Z, PRE_TOPC:64; :: thesis: f /" is continuous
g " is continuous by Z, TOPS_2:def 5;
hence f " is continuous by Z, PRE_TOPC:64; :: thesis: verum