let X be Banach_Algebra; :: thesis: for z being Point of X st ||.z.|| < 1 holds
( z GeoSeq is norm_summable & ||.(Sum (z GeoSeq)).|| <= 1 / (1 - ||.z.||) )
let z be Element of X; :: thesis: ( ||.z.|| < 1 implies ( z GeoSeq is norm_summable & ||.(Sum (z GeoSeq)).|| <= 1 / (1 - ||.z.||) ) )
A1: for n being Nat holds
( 0 <= ||.(z GeoSeq).|| . n & ||.(z GeoSeq).|| . n <= (||.z.|| GeoSeq) . n )

proof

defpred S₁[ Nat] means ( 0 <= ||.(z GeoSeq).|| . $1 & ||.(z GeoSeq).|| . $1 <= (||.z.|| GeoSeq) . $1 );
A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
||.(((z GeoSeq) . k) * z).|| <= ||.((z GeoSeq) . k).|| * ||.z.|| by LOPBAN_2:def 9;
then A4: ||.(((z GeoSeq) . k) * z).|| <= (||.(z GeoSeq).|| . k) * ||.z.|| by NORMSP_0:def 4;
assume S₁[k] ; :: thesis: S₁[k + 1]
then (||.(z GeoSeq).|| . k) * ||.z.|| <= ((||.z.|| GeoSeq) . k) * ||.z.|| by XREAL_1:64;
then A5: ||.(((z GeoSeq) . k) * z).|| <= ((||.z.|| GeoSeq) . k) * ||.z.|| by A4, XXREAL_0:2;
||.(z GeoSeq).|| . (k + 1) = ||.((z GeoSeq) . (k + 1)).|| by NORMSP_0:def 4
.= ||.(((z GeoSeq) . k) * z).|| by LOPBAN_3:def 9 ;
hence S₁[k + 1] by A5, PREPOWER:3; :: thesis: verum

end;

||.((z GeoSeq) . 0).|| = ||.(1. X).|| by LOPBAN_3:def 9
.= 1 by LOPBAN_2:def 10
.= (||.z.|| GeoSeq) . 0 by PREPOWER:3 ;
then A6: S₁[ 0 ] by NORMSP_0:def 4;
for n being Nat holds S₁[n] from NAT_1:sch 2(A6, A3);
hence for n being Nat holds
( 0 <= ||.(z GeoSeq).|| . n & ||.(z GeoSeq).|| . n <= (||.z.|| GeoSeq) . n ) ; :: thesis: verum

end;

assume ||.z.|| < 1 ; :: thesis: ( z GeoSeq is norm_summable & ||.(Sum (z GeoSeq)).|| <= 1 / (1 - ||.z.||) )
then |.||.z.||.| < 1 by ABSVALUE:def 1;
then A7: ( ||.z.|| GeoSeq is summable & Sum (||.z.|| GeoSeq) = 1 / (1 - ||.z.||) ) by SERIES_1:24;
then A8: ( ||.(z GeoSeq).|| is summable & Sum ||.(z GeoSeq).|| <= Sum (||.z.|| GeoSeq) ) by A1, SERIES_1:20;
z GeoSeq is norm_summable by A1, A7, SERIES_1:20;
then ||.(Sum (z GeoSeq)).|| <= Sum ||.(z GeoSeq).|| by LM0;
hence ( z GeoSeq is norm_summable & ||.(Sum (z GeoSeq)).|| <= 1 / (1 - ||.z.||) ) by A7, A8, XXREAL_0:2; :: thesis: verum