theorem LMTh3: :: NDIFF_9:16

for X, Y being non trivial RealBanachSpace
for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u is invertible holds
ex K, s being Real st
( 0 <= K & 0 < s & ( for du being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ||.du.|| < s holds
( u + du is invertible & ||.(((Inv (u + du)) - (Inv u)) - (- (((Inv u) * du) * (Inv u)))).|| <= K * (||.du.|| * ||.du.||) ) ) )