let X, Y be RealNormSpace; :: thesis: 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 )
let v be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis: ( v is invertible implies ( (Inv v) * v = id X & v * (Inv v) = id Y ) )
assume A1: v is invertible ; :: thesis: ( (Inv v) * v = id X & v * (Inv v) = id Y )
v is Lipschitzian LinearOperator of X,Y by LOPBAN_1:def 9;
then A7: ( dom v = the carrier of X & rng v = the carrier of Y ) by A1, FUNCT_2:def 1;
Inv v = v " by A1, Def1;
then A9: modetrans ((Inv v),Y,X) = v " by LOPBAN_1:def 11;
then A11: (Inv v) * v = (v ") * v by LOPBAN_1:def 11;
v * (Inv v) = v * (v ") by A9, LOPBAN_1:def 11;
hence ( (Inv v) * v = id X & v * (Inv v) = id Y ) by A1, A7, A11, FUNCT_1:39; :: thesis: verum