let a be real number ; :: thesis: for s being Real_Sequence st a <> 1 & ( for n being Element of NAT holds s . (n + 1) = a * (s . n) ) holds
for n being Element of 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 Element of NAT holds s . (n + 1) = a * (s . n) ) implies for n being Element of NAT holds (Partial_Sums s) . n = ((s . 0 ) * (1 - (a to_power (n + 1)))) / (1 - a) )
assume A1: ( a <> 1 & ( for n being Element of NAT holds s . (n + 1) = a * (s . n) ) ) ; :: thesis: for n being Element of NAT holds (Partial_Sums s) . n = ((s . 0 ) * (1 - (a to_power (n + 1)))) / (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;

now

let n be Element of 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 A4, SEQ_1:13
.= (s . 0 ) * ((1 - (a to_power (n + 1))) / (1 - a)) by A1, Th26
.= ((s . 0 ) * (1 - (a to_power (n + 1)))) / (1 - a) ; :: thesis: verum

end;

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