let n be Nat; :: thesis: for a being Real st a <> 1 holds
(Partial_Sums (a GeoSeq)) . n = (1 - (a to_power (n + 1))) / (1 - a)
let a be Real; :: thesis: ( a <> 1 implies (Partial_Sums (a GeoSeq)) . n = (1 - (a to_power (n + 1))) / (1 - a) )
defpred S₁[ Nat] means (Partial_Sums (a GeoSeq)) . $1 = (1 - (a to_power ($1 + 1))) / (1 - a);
assume a <> 1 ; :: thesis: (Partial_Sums (a GeoSeq)) . n = (1 - (a to_power (n + 1))) / (1 - a)
then A1: 1 - a <> 0 ;
A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume (Partial_Sums (a GeoSeq)) . n = (1 - (a to_power (n + 1))) / (1 - a) ; :: thesis: S₁[n + 1]
hence (Partial_Sums (a GeoSeq)) . (n + 1) = ((1 - (a to_power (n + 1))) / (1 - a)) + ((a GeoSeq) . (n + 1)) by Def1
.= ((1 - (a to_power (n + 1))) / (1 - a)) + ((a to_power (n + 1)) * 1) by PREPOWER:def 1
.= ((1 - (a to_power (n + 1))) / (1 - a)) + ((a to_power (n + 1)) * ((1 - a) / (1 - a))) by A1, XCMPLX_1:60
.= ((1 - (a to_power (n + 1))) / (1 - a)) + (((a to_power (n + 1)) * (1 - a)) / (1 - a))
.= ((1 - (a to_power (n + 1))) + ((a to_power (n + 1)) - ((a |^ (n + 1)) * a))) / (1 - a)
.= ((1 - (a to_power (n + 1))) + ((a to_power (n + 1)) - (a |^ ((n + 1) + 1)))) / (1 - a) by NEWTON:6
.= (1 - (a to_power ((n + 1) + 1))) / (1 - a) ;
:: thesis: verum

end;

(Partial_Sums (a GeoSeq)) . 0 = (a GeoSeq) . 0 by Def1
.= 1 by PREPOWER:3
.= (1 - a) / (1 - a) by A1, XCMPLX_1:60
.= (1 - (a to_power (0 + 1))) / (1 - a) ;
then A3: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A2);
hence (Partial_Sums (a GeoSeq)) . n = (1 - (a to_power (n + 1))) / (1 - a) ; :: thesis: verum