let X be 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) ) )
let v, I be Point of (R_NormSpace_of_BoundedLinearOperators (X,X)); ( I = id X & ||.v.|| < 1 implies ( 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) ) ) )
assume that
A1:
I = id X
and
A2:
||.v.|| < 1
; ( 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) ) )
set S = R_Normed_Algebra_of_BoundedLinearOperators X;
reconsider w = v as Point of (R_Normed_Algebra_of_BoundedLinearOperators X) ;
set x = (1. (R_Normed_Algebra_of_BoundedLinearOperators X)) + w;
||.w.|| < 1
by A2;
then A3:
( (1. (R_Normed_Algebra_of_BoundedLinearOperators X)) + w is invertible & (- w) GeoSeq is norm_summable & ((1. (R_Normed_Algebra_of_BoundedLinearOperators X)) + w) " = Sum ((- w) GeoSeq) & ||.(((1. (R_Normed_Algebra_of_BoundedLinearOperators X)) + w) ").|| <= 1 / (1 - ||.w.||) )
by LM2;
hence A6:
I + v is invertible
by A1, LM4; ( ||.(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) ) )
A7:
(I + v) " = ((1. (R_Normed_Algebra_of_BoundedLinearOperators X)) + w) "
by A1, A3, LM4;
hence
||.(Inv (I + v)).|| <= 1 / (1 - ||.v.||)
by A3, A6, Def1; 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) )
thus
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) )
by A3, A6, A7, Def1; verum