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

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

hence
f is one-to-one
by FUNCT_1:def 4; :: thesis: verumx = 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;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