let T be TopStruct ; :: thesis: for S being non empty TopStruct
for f being Function of T,S st f is being_homeomorphism holds
f " is being_homeomorphism
let S be non empty TopStruct ; :: thesis: for f being Function of T,S st f is being_homeomorphism holds
f " is being_homeomorphism
let f be Function of T,S; :: thesis: ( f is being_homeomorphism implies f " is being_homeomorphism )
assume A1: f is being_homeomorphism ; :: thesis: f " is being_homeomorphism
then A2: ( rng f = [#] S & f is one-to-one ) by Def5;
hence ( dom (f ") = [#] S & rng (f ") = [#] T ) by Th62; :: 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 A2, Th63; :: thesis: ( f " is continuous & (f ") " is continuous )
thus f " is continuous by A1, Def5; :: thesis: (f ") " is continuous
f is continuous by A1, Def5;
hence (f ") " is continuous by A2, Th64; :: thesis: verum