theorem LM60: :: LOPBAN13:15

for X, Y being non trivial RealBanachSpace
for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u is invertible holds
( Inv u is invertible & Inv (Inv u) = u )