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₁[ Nat] means s . $1 = (s . 0) * ((a GeoSeq) . $1);
A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be 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 Nat holds S₁[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;

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

let 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;

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