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: ( dom f = [#] T & rng f = [#] S & f is one-to-one & f is continuous & f " is continuous ) 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
thus (f " ) " is continuous by A2, Th64; :: thesis: verum