let f be Function of (TopSpaceMetr M),(TopSpaceMetr M); :: thesis: ( f is onto & f is isometric implies f is being_homeomorphism )
assume A1: ( f is onto & f is isometric ) ; :: thesis: f is being_homeomorphism
then reconsider f1 = f as onto isometric Function of (TopSpaceMetr M),(TopSpaceMetr M) ;
thus dom f = [#] (TopSpaceMetr M) by FUNCT_2:def 1; :: according to TOPS_2:def 5 :: thesis: ( rng f = [#] (TopSpaceMetr M) & f is one-to-one & f is continuous & f " is continuous )
consider g being isometric Function of M,M such that
A2: g = f by A1;
g is onto by A1, A2;
hence rng f = [#] (TopSpaceMetr M) by A2; :: thesis: ( f is one-to-one & f is continuous & f " is continuous )
thus f is one-to-one by A2; :: thesis: ( f is continuous & f " is continuous )
f1 is continuous ;
hence f is continuous ; :: thesis: f " is continuous
f " is isometric Function of (TopSpaceMetr M),(TopSpaceMetr M) by A1, Def2;
hence f " is continuous ; :: thesis: verum