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 that
A1: abs a < 1 and
A2: 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);
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 A2
.= (s . 0) * (((a GeoSeq) . n) * a)
.= (s . 0) * ((a GeoSeq) . (n + 1)) by PREPOWER:3 ;
hence S₁[n + 1] ; :: thesis: verum

end;

(a GeoSeq) . 0 = 1 by PREPOWER:3;
then A4: S₁[ 0 ] ;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A4, A3);
then s = (s . 0) (#) (a GeoSeq) by SEQ_1:9;
then A5: Partial_Sums s = (s . 0) (#) (Partial_Sums (a GeoSeq)) by Th12;
a GeoSeq is summable by A1, Th28;
then A6: Partial_Sums (a GeoSeq) is convergent by Def2;
then Partial_Sums s is convergent by A5;
hence s is summable by Def2; :: thesis: Sum s = (s . 0) / (1 - a)
Sum (a GeoSeq) = 1 / (1 - a) by A1, Th28;
then lim (Partial_Sums s) = (s . 0) * (1 / (1 - a)) by A5, A6, SEQ_2:8
.= ((s . 0) * 1) / (1 - a)
.= (s . 0) / (1 - a) ;
hence Sum s = (s . 0) / (1 - a) ; :: thesis: verum