let X, Y be non trivial RealBanachSpace; :: thesis: ex I being PartFunc of (R_NormSpace_of_BoundedLinearOperators (X,Y)),(R_NormSpace_of_BoundedLinearOperators (Y,X)) st
( dom I = InvertibleOperators (X,Y) & rng I = InvertibleOperators (Y,X) & I is one-to-one & I is_differentiable_on InvertibleOperators (X,Y) & ex J being PartFunc of (R_NormSpace_of_BoundedLinearOperators (Y,X)),(R_NormSpace_of_BoundedLinearOperators (X,Y)) st
( J = I " & J is one-to-one & dom J = InvertibleOperators (Y,X) & rng J = InvertibleOperators (X,Y) & J is_differentiable_on InvertibleOperators (Y,X) ) & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u in InvertibleOperators (X,Y) holds
I . u = Inv u ) & ( for u, du being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u in InvertibleOperators (X,Y) holds
(diff (I,u)) . du = - (((Inv u) * du) * (Inv u)) ) )
set S = R_NormSpace_of_BoundedLinearOperators (X,Y);
set K = R_NormSpace_of_BoundedLinearOperators (Y,X);
consider I being PartFunc of (R_NormSpace_of_BoundedLinearOperators (X,Y)),(R_NormSpace_of_BoundedLinearOperators (Y,X)) such that
A1: ( dom I = InvertibleOperators (X,Y) & rng I = InvertibleOperators (Y,X) & I is one-to-one & I is_continuous_on InvertibleOperators (X,Y) & ex J being PartFunc of (R_NormSpace_of_BoundedLinearOperators (Y,X)),(R_NormSpace_of_BoundedLinearOperators (X,Y)) st
( J = I " & J is one-to-one & dom J = InvertibleOperators (Y,X) & rng J = InvertibleOperators (X,Y) & J is_continuous_on InvertibleOperators (Y,X) ) & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u in InvertibleOperators (X,Y) holds
I . u = Inv u ) ) by LOPBAN13:25;
consider J being PartFunc of (R_NormSpace_of_BoundedLinearOperators (Y,X)),(R_NormSpace_of_BoundedLinearOperators (X,Y)) such that
A2: ( J = I " & J is one-to-one & dom J = InvertibleOperators (Y,X) & rng J = InvertibleOperators (X,Y) & J is_continuous_on InvertibleOperators (Y,X) ) by A1;
take I ; :: thesis: ( dom I = InvertibleOperators (X,Y) & rng I = InvertibleOperators (Y,X) & I is one-to-one & I is_differentiable_on InvertibleOperators (X,Y) & ex J being PartFunc of (R_NormSpace_of_BoundedLinearOperators (Y,X)),(R_NormSpace_of_BoundedLinearOperators (X,Y)) st
( J = I " & J is one-to-one & dom J = InvertibleOperators (Y,X) & rng J = InvertibleOperators (X,Y) & J is_differentiable_on InvertibleOperators (Y,X) ) & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u in InvertibleOperators (X,Y) holds
I . u = Inv u ) & ( for u, du being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u in InvertibleOperators (X,Y) holds
(diff (I,u)) . du = - (((Inv u) * du) * (Inv u)) ) )
A4: for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u in InvertibleOperators (X,Y) holds
I is_differentiable_in u by A1, LM80;
for v being Point of (R_NormSpace_of_BoundedLinearOperators (Y,X)) st v in InvertibleOperators (Y,X) holds
J . v = Inv v

proof

let v be Point of (R_NormSpace_of_BoundedLinearOperators (Y,X)); :: thesis: ( v in InvertibleOperators (Y,X) implies J . v = Inv v )
assume v in InvertibleOperators (Y,X) ; :: thesis: J . v = Inv v
then consider u being object such that
A5: ( u in dom I & v = I . u ) by A1, FUNCT_1:def 3;
reconsider u = u as Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) by A5;
A7: ex u0 being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st
( u = u0 & u0 is invertible ) by A1, A5;
thus J . v = u by A1, A2, A5, FUNCT_1:34
.= Inv (Inv u) by A7, LOPBAN13:15
.= Inv v by A1, A5 ; :: thesis: verum

end;

then for v being Point of (R_NormSpace_of_BoundedLinearOperators (Y,X)) st v in InvertibleOperators (Y,X) holds
J is_differentiable_in v by A2, LM80;
then J is_differentiable_on InvertibleOperators (Y,X) by A2, NDIFF_1:31;
hence ( dom I = InvertibleOperators (X,Y) & rng I = InvertibleOperators (Y,X) & I is one-to-one & I is_differentiable_on InvertibleOperators (X,Y) & ex J being PartFunc of (R_NormSpace_of_BoundedLinearOperators (Y,X)),(R_NormSpace_of_BoundedLinearOperators (X,Y)) st
( J = I " & J is one-to-one & dom J = InvertibleOperators (Y,X) & rng J = InvertibleOperators (X,Y) & J is_differentiable_on InvertibleOperators (Y,X) ) & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u in InvertibleOperators (X,Y) holds
I . u = Inv u ) & ( for u, du being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u in InvertibleOperators (X,Y) holds
(diff (I,u)) . du = - (((Inv u) * du) * (Inv u)) ) ) by A1, A2, A4, LM80, NDIFF_1:31; :: thesis: verum