let a be Real; :: thesis: for s being Real_Sequence st a <> 1 & a <> 0 & ( for n being Nat holds s . n = (1 / a) |^ n ) holds
for n being Nat holds (Partial_Sums s) . n = (((1 / a) |^ n) - a) / (1 - a)
let s be Real_Sequence; :: thesis: ( a <> 1 & a <> 0 & ( for n being Nat holds s . n = (1 / a) |^ n ) implies for n being Nat holds (Partial_Sums s) . n = (((1 / a) |^ n) - a) / (1 - a) )
assume that
A1: a <> 1 and
A2: a <> 0 ; :: thesis: ( ex n being Nat st not s . n = (1 / a) |^ n or for n being Nat holds (Partial_Sums s) . n = (((1 / a) |^ n) - a) / (1 - a) )
defpred S₁[ Nat] means (Partial_Sums s) . $1 = (((1 / a) |^ $1) - a) / (1 - a);
assume A3: for n being Nat holds s . n = (1 / a) |^ n ; :: thesis: for n being Nat holds (Partial_Sums s) . n = (((1 / a) |^ n) - a) / (1 - a)
A4: 1 - a <> 0 by A1;
A5: 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 s) . n = (((1 / a) |^ n) - a) / (1 - a) ; :: thesis: S₁[n + 1]
hence (Partial_Sums s) . (n + 1) = ((((1 / a) |^ n) - a) / (1 - a)) + (s . (n + 1)) by SERIES_1:def 1
.= ((((1 / a) |^ n) - a) / (1 - a)) + (((1 / a) |^ (n + 1)) * 1) by A3
.= ((((1 / a) |^ n) - a) / (1 - a)) + (((1 / a) |^ (n + 1)) * ((1 - a) / (1 - a))) by A4, XCMPLX_1:60
.= ((((1 / a) |^ n) - a) / (1 - a)) + ((((1 / a) |^ (n + 1)) * (1 - a)) / (1 - a)) by XCMPLX_1:74
.= ((((1 / a) |^ n) - a) + ((((1 / a) |^ (n + 1)) * 1) - (((1 / a) |^ (n + 1)) * a))) / (1 - a) by XCMPLX_1:62
.= (((((1 / a) |^ n) - a) + ((1 / a) |^ (n + 1))) - (((1 / a) |^ (n + 1)) * a)) / (1 - a)
.= (((((1 / a) |^ n) - a) + ((1 / a) |^ (n + 1))) - ((((1 / a) |^ n) * (1 / a)) * a)) / (1 - a) by NEWTON:6
.= (((((1 / a) |^ n) - a) + ((1 / a) |^ (n + 1))) - (((1 / a) |^ n) * ((1 / a) * a))) / (1 - a)
.= (((((1 / a) |^ n) - a) + ((1 / a) |^ (n + 1))) - (((1 / a) |^ n) * 1)) / (1 - a) by A2, XCMPLX_1:106
.= (((1 / a) |^ (n + 1)) - a) / (1 - a) ;
:: thesis: verum

end;

(Partial_Sums s) . 0 = s . 0 by SERIES_1:def 1
.= (1 / a) |^ 0 by A3
.= 1 by NEWTON:4
.= (1 - a) / (1 - a) by A4, XCMPLX_1:60
.= (((1 / a) |^ 0) - a) / (1 - a) by NEWTON:4 ;
then A6: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A6, A5);
hence for n being Nat holds (Partial_Sums s) . n = (((1 / a) |^ n) - a) / (1 - a) ; :: thesis: verum