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 ) )
assume A1: ||.z.|| < 1 ; :: thesis: ( z GeoSeq is summable & z GeoSeq is norm_summable )
0 <= ||.z.|| by CLVECT_1:106;
then A2: abs ||.z.|| < 1 by A1, ABSVALUE:def 1;
A3: 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 );
A4: ||.(z GeoSeq ).|| . 0 = ||.((z GeoSeq ) . 0 ).|| by CLVECT_1:def 17;
||.((z GeoSeq ) . 0 ).|| = ||.(1. X).|| by Def12
.= 1 by CLOPBAN2:def 10
.= (||.z.|| GeoSeq ) . 0 by PREPOWER:4 ;
then A5: S₁[ 0 ] by A4, CLVECT_1:106;
A6: 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] )
assume A7: S₁[k] ; :: thesis: S₁[k + 1]
A8: 0 <= ||.z.|| by CLVECT_1:106;
A9: ||.(z GeoSeq ).|| . (k + 1) = ||.((z GeoSeq ) . (k + 1)).|| by CLVECT_1:def 17
.= ||.(((z GeoSeq ) . k) * z).|| by Def12 ;
||.(((z GeoSeq ) . k) * z).|| <= ||.((z GeoSeq ) . k).|| * ||.z.|| by CLOPBAN2:def 9;
then A10: ||.(((z GeoSeq ) . k) * z).|| <= (||.(z GeoSeq ).|| . k) * ||.z.|| by CLVECT_1:def 17;
(||.(z GeoSeq ).|| . k) * ||.z.|| <= ((||.z.|| GeoSeq ) . k) * ||.z.|| by A7, A8, XREAL_1:66;
then ||.(((z GeoSeq ) . k) * z).|| <= ((||.z.|| GeoSeq ) . k) * ||.z.|| by A10, XXREAL_0:2;
hence S₁[k + 1] by A9, CLVECT_1:106, PREPOWER:4; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A5, A6);
hence for n being Element of NAT holds
( 0 <= ||.(z GeoSeq ).|| . n & ||.(z GeoSeq ).|| . n <= (||.z.|| GeoSeq ) . n ) ; :: thesis: verum

end;

||.z.|| GeoSeq is summable by A2, SERIES_1:28;
then ||.(z GeoSeq ).|| is summable by A3, SERIES_1:24;
then z GeoSeq is norm_summable by Def4;
hence ( z GeoSeq is summable & z GeoSeq is norm_summable ) ; :: thesis: verum