theorem LMMAZU: :: NDIFF_7:7

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