let f be Function of (TopSpaceMetr M),(TopSpaceMetr M); :: thesis: ( f is isometric implies f is being_homeomorphism )
assume A1: f is isometric ; :: thesis: f is being_homeomorphism
then reconsider f1 = f as 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, Def2;
thus rng f = [#] (TopSpaceMetr M) by A2, VECTMETR:def 3; :: 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
g " is isometric Function of M,M by VECTMETR:3;
then f " is isometric Function of (TopSpaceMetr M),(TopSpaceMetr M) by A2, Def2;
hence f " is continuous ; :: thesis: verum