theorem LMTh2: :: LOPBAN13:17

for X, Y being non trivial RealBanachSpace
for u, v being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u is invertible & ||.(v - u).|| < 1 / ||.(Inv u).|| holds
( v is invertible & ||.(Inv v).|| <= 1 / ((1 / ||.(Inv u).||) - ||.(v - u).||) & ex w being Point of (R_Normed_Algebra_of_BoundedLinearOperators X) ex s, I being Point of (R_NormSpace_of_BoundedLinearOperators (X,X)) st
( w = (Inv u) * (v - u) & s = w & I = id X & ||.s.|| < 1 & (- w) GeoSeq is norm_summable & I + s is invertible & ||.(Inv (I + s)).|| <= 1 / (1 - ||.s.||) & Inv (I + s) = Sum ((- w) GeoSeq) & Inv v = (Inv (I + s)) * (Inv u) ) )