let X be Banach_Algebra; :: thesis: for z being Element of X st < 1 holds
( z GeoSeq is summable & z GeoSeq is norm_summable )

let z be Element of X; :: thesis: ( < 1 implies ( z GeoSeq is summable & z GeoSeq is norm_summable ) )
A1: for n being Nat holds
( 0 <= ||.().|| . n & ||.().|| . n <= () . n )
proof
defpred S1[ Nat] means ( 0 <= ||.().|| . \$1 & ||.().|| . \$1 <= () . \$1 );
A2: ||.().|| . 0 = ||.(() . 0).|| by NORMSP_0:def 4;
A3: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
||.((() . k) * z).|| <= ||.(() . k).|| * by LOPBAN_2:def 9;
then A4: ||.((() . k) * z).|| <= (||.().|| . k) * by NORMSP_0:def 4;
assume S1[k] ; :: thesis: S1[k + 1]
then (||.().|| . k) * <= (() . k) * by XREAL_1:64;
then A5: ||.((() . k) * z).|| <= (() . k) * by ;
||.().|| . (k + 1) = ||.(() . (k + 1)).|| by NORMSP_0:def 4
.= ||.((() . k) * z).|| by Def9 ;
hence S1[k + 1] by ; :: thesis: verum
end;
||.(() . 0).|| = ||.(1. X).|| by Def9
.= 1 by LOPBAN_2:def 10
.= () . 0 by PREPOWER:3 ;
then A6: S1[ 0 ] by A2;
for n being Nat holds S1[n] from NAT_1:sch 2(A6, A3);
hence for n being Nat holds
( 0 <= ||.().|| . n & ||.().|| . n <= () . n ) ; :: thesis: verum
end;
assume ||.z.|| < 1 ; :: thesis: ( z GeoSeq is summable & z GeoSeq is norm_summable )
then |..| < 1 by ABSVALUE:def 1;
then ||.z.|| GeoSeq is summable by SERIES_1:24;
then ||.().|| is summable by ;
then z GeoSeq is norm_summable ;
hence ( z GeoSeq is summable & z GeoSeq is norm_summable ) ; :: thesis: verum