theorem LM400: :: LOPBAN13:22

for X, Y being RealNormSpace
for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u is invertible holds
( (Inv u) * u = id X & u * (Inv u) = id Y )