theorem LMX00: :: NDIFF_7:22

for S, T, W being RealNormSpace
for f being Point of (R_NormSpace_of_BoundedLinearOperators (S,W))
for g being Point of (R_NormSpace_of_BoundedLinearOperators (T,W))
for I being LinearOperator of S,T st I is one-to-one & I is onto & I is isometric & f = g * I holds
||.f.|| = ||.g.||