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 consider g being isometric Function of M,M such that
A2: g = f by Def2;
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 )
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 )
reconsider f1 = f as isometric Function of (TopSpaceMetr M),(TopSpaceMetr M) by A1;
f1 is continuous ;
hence f is continuous ; :: thesis: f /" is continuous
A3: g " is isometric Function of M,M by VECTMETR:3;
f " is isometric Function of (TopSpaceMetr M),(TopSpaceMetr M) by A2, A3, Def2;
hence f /" is continuous ; :: thesis: verum