let a be Real; :: thesis: for s being Real_Sequence st |.a.| < 1 & ( for n being Nat holds s . (n + 1) = a * (s . n) ) holds

( s is summable & Sum s = (s . 0) / (1 - a) )

let s be Real_Sequence; :: thesis: ( |.a.| < 1 & ( for n being Nat holds s . (n + 1) = a * (s . n) ) implies ( s is summable & Sum s = (s . 0) / (1 - a) ) )

assume that

A1: |.a.| < 1 and

A2: for n being Nat holds s . (n + 1) = a * (s . n) ; :: thesis: ( s is summable & Sum s = (s . 0) / (1 - a) )

defpred S_{1}[ Nat] means s . $1 = (s . 0) * ((a GeoSeq) . $1);

A3: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]

then A4: S_{1}[ 0 ]
;

for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A4, A3);

then s = (s . 0) (#) (a GeoSeq) by SEQ_1:9;

then A5: Partial_Sums s = (s . 0) (#) (Partial_Sums (a GeoSeq)) by Th9;

a GeoSeq is summable by A1, Th24;

then A6: Partial_Sums (a GeoSeq) is convergent ;

then Partial_Sums s is convergent by A5;

hence s is summable ; :: thesis: Sum s = (s . 0) / (1 - a)

Sum (a GeoSeq) = 1 / (1 - a) by A1, Th24;

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

( s is summable & Sum s = (s . 0) / (1 - a) )

let s be Real_Sequence; :: thesis: ( |.a.| < 1 & ( for n being Nat holds s . (n + 1) = a * (s . n) ) implies ( s is summable & Sum s = (s . 0) / (1 - a) ) )

assume that

A1: |.a.| < 1 and

A2: for n being Nat holds s . (n + 1) = a * (s . n) ; :: thesis: ( s is summable & Sum s = (s . 0) / (1 - a) )

defpred S

A3: for n being Nat st S

S

proof

(a GeoSeq) . 0 = 1
by PREPOWER:3;
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume s . n = (s . 0) * ((a GeoSeq) . n) ; :: thesis: S_{1}[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_{1}[n + 1]
; :: thesis: verum

end;assume s . n = (s . 0) * ((a GeoSeq) . n) ; :: thesis: S

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

then A4: S

for n being Nat holds S

then s = (s . 0) (#) (a GeoSeq) by SEQ_1:9;

then A5: Partial_Sums s = (s . 0) (#) (Partial_Sums (a GeoSeq)) by Th9;

a GeoSeq is summable by A1, Th24;

then A6: Partial_Sums (a GeoSeq) is convergent ;

then Partial_Sums s is convergent by A5;

hence s is summable ; :: thesis: Sum s = (s . 0) / (1 - a)

Sum (a GeoSeq) = 1 / (1 - a) by A1, Th24;

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