:: deftheorem defines invertible LOPBAN13:def 1 :
for X, Y being RealNormSpace
for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds
( u is invertible iff ( u is one-to-one & rng u = the carrier of Y & u " is Point of (R_NormSpace_of_BoundedLinearOperators (Y,X)) ) );