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