let X be 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: 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 );
A2: ||.(z GeoSeq).|| . 0 = ||.((z GeoSeq) . 0).|| by NORMSP_0:def 4;
A3: 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] )
||.(((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 Def9 ;
hence S₁[k + 1] by A5, PREPOWER:3; :: thesis: verum

end;

||.((z GeoSeq) . 0).|| = ||.(1. X).|| by Def9
.= 1 by LOPBAN_2:def 10
.= (||.z.|| GeoSeq) . 0 by PREPOWER:3 ;
then A6: S₁[ 0 ] by A2;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A6, A3);
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 ABSVALUE:def 1;
then ||.z.|| GeoSeq is summable by SERIES_1:24;
then ||.(z GeoSeq).|| is summable by A1, SERIES_1:20;
then z GeoSeq is norm_summable by Def3;
hence ( z GeoSeq is summable & z GeoSeq is norm_summable ) ; :: thesis: verum