let a be real number ; :: thesis: for s being Real_Sequence st abs a < 1 & ( for n being Element of NAT holds s . (n + 1) = a * (s . n) ) holds
( s is summable & Sum s = (s . 0 ) / (1 - a) )
let s be Real_Sequence; :: thesis: ( abs a < 1 & ( for n being Element of NAT holds s . (n + 1) = a * (s . n) ) implies ( s is summable & Sum s = (s . 0 ) / (1 - a) ) )
assume A1: ( abs a < 1 & ( for n being Element of NAT holds s . (n + 1) = a * (s . n) ) ) ; :: thesis: ( s is summable & Sum s = (s . 0 ) / (1 - a) )
defpred S₁[ Element of NAT ] means s . $1 = (s . 0 ) * ((a GeoSeq ) . $1);
(a GeoSeq ) . 0 = 1 by PREPOWER:4;
then A2: S₁[ 0 ] ;
A3: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume s . n = (s . 0 ) * ((a GeoSeq ) . n) ; :: thesis: S₁[n + 1]
then s . (n + 1) = a * ((s . 0 ) * ((a GeoSeq ) . n)) by A1
.= (s . 0 ) * (((a GeoSeq ) . n) * a)
.= (s . 0 ) * ((a GeoSeq ) . (n + 1)) by PREPOWER:4 ;
hence S₁[n + 1] ; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A2, A3);
then s = (s . 0 ) (#) (a GeoSeq ) by SEQ_1:13;
then A4: Partial_Sums s = (s . 0 ) (#) (Partial_Sums (a GeoSeq )) by Th12;
A5: ( a GeoSeq is summable & Sum (a GeoSeq ) = 1 / (1 - a) ) by A1, Th28;
then A6: Partial_Sums (a GeoSeq ) is convergent by Def2;
then A7: Partial_Sums s is convergent by A4, SEQ_2:21;
A8: lim (Partial_Sums s) = (s . 0 ) * (1 / (1 - a)) by A4, A5, A6, SEQ_2:22
.= ((s . 0 ) * 1) / (1 - a)
.= (s . 0 ) / (1 - a) ;
thus s is summable by A7, Def2; :: thesis: Sum s = (s . 0 ) / (1 - a)
thus Sum s = (s . 0 ) / (1 - a) by A8; :: thesis: verum