theorem LM80:
for
X,
Y being non
trivial RealBanachSpace for
I being
PartFunc of
(R_NormSpace_of_BoundedLinearOperators (X,Y)),
(R_NormSpace_of_BoundedLinearOperators (Y,X)) st
dom I = InvertibleOperators (
X,
Y) & ( for
u being
Point of
(R_NormSpace_of_BoundedLinearOperators (X,Y)) st
u in InvertibleOperators (
X,
Y) holds
I . u = Inv u ) holds
for
u being
Point of
(R_NormSpace_of_BoundedLinearOperators (X,Y)) st
u in InvertibleOperators (
X,
Y) holds
(
I is_differentiable_in u & ( for
du being
Point of
(R_NormSpace_of_BoundedLinearOperators (X,Y)) holds
(diff (I,u)) . du = - (((Inv u) * du) * (Inv u)) ) )