let X be Complex_Banach_Algebra; :: thesis: for z being Element of X st ||.z.|| < 1 holds
( z GeoSeq is summable & z GeoSeq is norm_summable )
let z be Element of X; :: thesis: ( ||.z.|| < 1 implies ( z GeoSeq is summable & z GeoSeq is norm_summable ) )
A1: 0 <= ||.z.|| by CLVECT_1:105;
A2: for n being Element of NAT holds
( 0 <= ||.(z GeoSeq).|| . n & ||.(z GeoSeq).|| . n <= (||.z.|| GeoSeq) . n )

proof

defpred S₁[ Element of NAT ] means ( 0 <= ||.(z GeoSeq).|| . $1 & ||.(z GeoSeq).|| . $1 <= (||.z.|| GeoSeq) . $1 );
A3: ||.(z GeoSeq).|| . 0 = ||.((z GeoSeq) . 0).|| by NORMSP_0:def 4;
A4: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
A5: 0 <= ||.z.|| by CLVECT_1:105;
||.(((z GeoSeq) . k) * z).|| <= ||.((z GeoSeq) . k).|| * ||.z.|| by CLOPBAN2:def 9;
then A6: ||.(((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 A5, XREAL_1:64;
then A7: ||.(((z GeoSeq) . k) * z).|| <= ((||.z.|| GeoSeq) . k) * ||.z.|| by A6, XXREAL_0:2;
||.(z GeoSeq).|| . (k + 1) = ||.((z GeoSeq) . (k + 1)).|| by NORMSP_0:def 4
.= ||.(((z GeoSeq) . k) * z).|| by Def12 ;
hence S₁[k + 1] by A7, CLVECT_1:105, PREPOWER:3; :: thesis: verum

end;

||.((z GeoSeq) . 0).|| = ||.(1. X).|| by Def12
.= 1 by CLOPBAN2:def 10
.= (||.z.|| GeoSeq) . 0 by PREPOWER:3 ;
then A8: S₁[ 0 ] by A3, CLVECT_1:105;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A8, A4);
hence for n being Element of NAT holds
( 0 <= ||.(z GeoSeq).|| . n & ||.(z GeoSeq).|| . n <= (||.z.|| GeoSeq) . n ) ; :: thesis: verum

end;

assume ||.z.|| < 1 ; :: thesis: ( z GeoSeq is summable & z GeoSeq is norm_summable )
then abs ||.z.|| < 1 by A1, ABSVALUE:def 1;
then ||.z.|| GeoSeq is summable by SERIES_1:24;
then ||.(z GeoSeq).|| is summable by A2, SERIES_1:20;
then z GeoSeq is norm_summable by Def4;
hence ( z GeoSeq is summable & z GeoSeq is norm_summable ) ; :: thesis: verum