let X, Y be non trivial RealBanachSpace; :: thesis: for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u is invertible holds
( Inv u is invertible & Inv (Inv u) = u )
let u be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis: ( u is invertible implies ( Inv u is invertible & Inv (Inv u) = u ) )
assume A1: u is invertible ; :: thesis: ( Inv u is invertible & Inv (Inv u) = u )
then A3: Inv u = u " by Def1;
reconsider Lu = u as Lipschitzian LinearOperator of X,Y by LOPBAN_1:def 9;
A5: rng (Inv u) = dom Lu by A1, A3, FUNCT_1:33
.= the carrier of X by FUNCT_2:def 1 ;
A6: (Inv u) " = u by A1, A3, FUNCT_1:43;
thus Inv u is invertible by A1, A3, A5, FUNCT_1:43; :: thesis: Inv (Inv u) = u
hence Inv (Inv u) = u by A6, Def1; :: thesis: verum