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 :: thesis: for x, y being object st x in dom f & y in dom f & f . x = f . y holds
x = y
let x, y be object ; :: thesis: ( x in dom f & y in dom f & f . x = f . y implies x = y )
assume that
A2: ( x in dom f & y in dom f ) and
A3: f . x = f . y ; :: thesis: x = y
reconsider x1 = x, y1 = y as Element of V by A2;
dist (x1,y1) = dist ((f . x1),(f . y1)) by A1
.= 0 by A3, METRIC_1:1 ;
hence x = y by METRIC_1:2; :: thesis: verum
end;
hence f is one-to-one by FUNCT_1:def 4; :: thesis: verum