let S be Banach_Algebra; :: thesis: for w being Point of S st ||.w.|| < 1 holds
( (1. S) + w is invertible & (- w) GeoSeq is norm_summable & ((1. S) + w) " = Sum ((- w) GeoSeq) & ||.(((1. S) + w) ").|| <= 1 / (1 - ||.w.||) )
let w be Point of S; :: thesis: ( ||.w.|| < 1 implies ( (1. S) + w is invertible & (- w) GeoSeq is norm_summable & ((1. S) + w) " = Sum ((- w) GeoSeq) & ||.(((1. S) + w) ").|| <= 1 / (1 - ||.w.||) ) )
assume A1: ||.w.|| < 1 ; :: thesis: ( (1. S) + w is invertible & (- w) GeoSeq is norm_summable & ((1. S) + w) " = Sum ((- w) GeoSeq) & ||.(((1. S) + w) ").|| <= 1 / (1 - ||.w.||) )
set x = (1. S) + w;
A2: ||.((1. S) - ((1. S) + w)).|| = ||.(((1. S) + w) - (1. S)).|| by NORMSP_1:7
.= ||.w.|| by RLVECT_4:1 ;
then A3: ( (1. S) + w is invertible & ((1. S) + w) " = Sum (((1. S) - ((1. S) + w)) GeoSeq) ) by A1, LOPBAN_3:42;
(1. S) - ((1. S) + w) = ((1. S) - (1. S)) - w by RLVECT_1:27
.= (0. S) - w by RLVECT_1:15
.= - w by RLVECT_1:14 ;
hence ( (1. S) + w is invertible & (- w) GeoSeq is norm_summable & ((1. S) + w) " = Sum ((- w) GeoSeq) & ||.(((1. S) + w) ").|| <= 1 / (1 - ||.w.||) ) by A1, A2, A3, LM1; :: thesis: verum