let f be Function of S,T; :: thesis: ( f is being_homeomorphism implies ( f is onto & f is one-to-one & f is continuous ) )
assume A1: f is being_homeomorphism ; :: thesis: ( f is onto & f is one-to-one & f is continuous )
then ( rng f = [#] T & dom f = [#] S ) by TOPS_2:def 5;
hence rng f = the carrier of T ; :: according to FUNCT_2:def 3 :: thesis: ( f is one-to-one & f is continuous )
thus ( f is one-to-one & f is continuous ) by A1, TOPS_2:def 5; :: thesis: verum