for X, Y being non trivial RealBanachSpace ex I being Function of (InvertibleOperators (X,Y)),(InvertibleOperators (Y,X)) st
( I is one-to-one & I is onto & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u in InvertibleOperators (X,Y) holds
I . u = Inv u ) )