:: deftheorem Def1 defines Inv LOPBAN13:def 2 :
for X, Y being RealNormSpace
for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u is invertible holds
Inv u = u " ;