let V be non empty Reflexive discerning MetrStruct ; :: thesis: for f being Function of V,V st f is isometric holds
f is one-to-one
let f be Function of V,V; :: thesis: ( f is isometric implies f is one-to-one )
assume A1: f is isometric ; :: thesis: f is one-to-one

now

let x, y be set ; :: thesis: ( x in dom f & y in dom f & f . x = f . y implies x = y )
assume that
A2: x in dom f and
A3: y in dom f and
A4: f . x = f . y ; :: thesis: x = y
reconsider x1 = x, y1 = y as Element of V by A2, A3;
dist x1,y1 = dist (f . x1),(f . y1) by A1, Def3
.= 0 by A4, METRIC_1:1 ;
hence x = y by METRIC_1:2; :: thesis: verum

end;

hence f is one-to-one by FUNCT_1:def 8; :: thesis: verum