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

for n being Nat holds (Partial_Sums s) . n = ((s . 0) * (1 - (a to_power (n + 1)))) / (1 - a)

let s be Real_Sequence; :: thesis: ( a <> 1 & ( for n being Nat holds s . (n + 1) = a * (s . n) ) implies for n being Nat holds (Partial_Sums s) . n = ((s . 0) * (1 - (a to_power (n + 1)))) / (1 - a) )

assume that

A1: a <> 1 and

A2: for n being Nat holds s . (n + 1) = a * (s . n) ; :: thesis: for n being Nat holds (Partial_Sums s) . n = ((s . 0) * (1 - (a to_power (n + 1)))) / (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;

for n being Nat holds (Partial_Sums s) . n = ((s . 0) * (1 - (a to_power (n + 1)))) / (1 - a)

let s be Real_Sequence; :: thesis: ( a <> 1 & ( for n being Nat holds s . (n + 1) = a * (s . n) ) implies for n being Nat holds (Partial_Sums s) . n = ((s . 0) * (1 - (a to_power (n + 1)))) / (1 - a) )

assume that

A1: a <> 1 and

A2: for n being Nat holds s . (n + 1) = a * (s . n) ; :: thesis: for n being Nat holds (Partial_Sums s) . n = ((s . 0) * (1 - (a to_power (n + 1)))) / (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;

now :: thesis: for n being Nat holds (Partial_Sums s) . n = ((s . 0) * (1 - (a to_power (n + 1)))) / (1 - a)

hence
for n being Nat holds (Partial_Sums s) . n = ((s . 0) * (1 - (a to_power (n + 1)))) / (1 - a)
; :: thesis: verumlet n be Nat; :: thesis: (Partial_Sums s) . n = ((s . 0) * (1 - (a to_power (n + 1)))) / (1 - a)

thus (Partial_Sums s) . n = (s . 0) * ((Partial_Sums (a GeoSeq)) . n) by A5, SEQ_1:9

.= (s . 0) * ((1 - (a to_power (n + 1))) / (1 - a)) by A1, Th22

.= ((s . 0) * (1 - (a to_power (n + 1)))) / (1 - a) ; :: thesis: verum

end;thus (Partial_Sums s) . n = (s . 0) * ((Partial_Sums (a GeoSeq)) . n) by A5, SEQ_1:9

.= (s . 0) * ((1 - (a to_power (n + 1))) / (1 - a)) by A1, Th22

.= ((s . 0) * (1 - (a to_power (n + 1)))) / (1 - a) ; :: thesis: verum