let S, T be RealNormSpace; :: thesis: for f being LinearOperator of S,T holds
( f is isometric iff for x being Element of S holds ||.(f . x).|| = ||.x.|| )
let f be LinearOperator of S,T; :: thesis: ( f is isometric iff for x being Element of S holds ||.(f . x).|| = ||.x.|| )

hereby :: thesis: ( ( for x being Element of S holds ||.(f . x).|| = ||.x.|| ) implies f is isometric )

assume A1: f is isometric ; :: thesis: for x being Element of S holds ||.(f . x).|| = ||.x.||
thus for x being Element of S holds ||.(f . x).|| = ||.x.|| :: thesis: verum

proof

let x be Element of S; :: thesis: ||.(f . x).|| = ||.x.||
thus ||.(f . x).|| = ||.(f . (x - (0. S))).|| by RLVECT_1:13
.= ||.((f . x) - (f . (0. S))).|| by LM001
.= ||.(x - (0. S)).|| by A1
.= ||.x.|| by RLVECT_1:13 ; :: thesis: verum

end;

end;

assume A2: for x being Element of S holds ||.(f . x).|| = ||.x.|| ; :: thesis: f is isometric
for a, b being Point of S holds ||.((f . a) - (f . b)).|| = ||.(a - b).||

proof

let a, b be Point of S; :: thesis: ||.((f . a) - (f . b)).|| = ||.(a - b).||
thus ||.((f . a) - (f . b)).|| = ||.(f . (a - b)).|| by LM001
.= ||.(a - b).|| by A2 ; :: thesis: verum

end;

hence f is isometric ; :: thesis: verum