theorem Th2: :: LOPBAN13:13

for X, Y being non trivial RealBanachSpace
for u, v being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u is invertible & ||.v.|| < 1 / ||.(Inv u).|| holds
( u + v is invertible & ||.(Inv (u + v)).|| <= 1 / ((1 / ||.(Inv u).||) - ||.v.||) & 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 & 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 (u + v) = (Inv (I + s)) * (Inv u) ) )