let f be Function of (TopSpaceMetr M),(TopSpaceMetr M); :: thesis: ( f is isometric implies f is continuous )
assume f is isometric ; :: thesis: f is continuous
then consider g being isometric Function of M,M such that
A1: g = f by Def2;
let W be Point of (TopSpaceMetr M); :: according to BORSUK_1:def 3 :: thesis: for b₁ being a_neighborhood of f . W ex b₂ being a_neighborhood of W st f .: b₂ c= b₁
let G be a_neighborhood of f . W; :: thesis: ex b₁ being a_neighborhood of W st f .: b₁ c= G
reconsider fw = f . W, w = W as Point of M ;
f . W in Int G by CONNSP_2:def 1;
then consider r being real number such that
A2: ( r > 0 & Ball fw,r c= G ) by GOBOARD6:7;
reconsider H = Ball w,r as a_neighborhood of W by A2, GOBOARD6:94;
take H ; :: thesis: f .: H c= G
thus f .: H c= G :: thesis: verum

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in f .: H or a in G )
assume a in f .: H ; :: thesis: a in G
then consider b being set such that
A3: ( b in dom f & b in H & f . b = a ) by FUNCT_1:def 12;
reconsider b = b as Point of (TopSpaceMetr M) by A3;
reconsider b' = b as Point of M ;
dist b',w < r by A3, METRIC_1:12;
then dist (g . b'),fw < r by A1, VECTMETR:def 3;
then a in Ball fw,r by A1, A3, METRIC_1:12;
hence a in G by A2; :: thesis: verum

end;