let n be Nat; :: thesis: for a being Real
for s being Real_Sequence st a <> 1 & ( for n being Nat holds s . n = a |^ n ) holds
() . n = (1 - (a |^ (n + 1))) / (1 - a)

let a be Real; :: thesis: for s being Real_Sequence st a <> 1 & ( for n being Nat holds s . n = a |^ n ) holds
() . n = (1 - (a |^ (n + 1))) / (1 - a)

let s be Real_Sequence; :: thesis: ( a <> 1 & ( for n being Nat holds s . n = a |^ n ) implies () . n = (1 - (a |^ (n + 1))) / (1 - a) )
defpred S1[ Nat] means () . \$1 = (1 - (a |^ (\$1 + 1))) / (1 - a);
assume a <> 1 ; :: thesis: ( ex n being Nat st not s . n = a |^ n or () . n = (1 - (a |^ (n + 1))) / (1 - a) )
then A1: 1 - a <> 0 ;
assume A2: for n being Nat holds s . n = a |^ n ; :: thesis: () . n = (1 - (a |^ (n + 1))) / (1 - a)
A3: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume (Partial_Sums s) . n = (1 - (a |^ (n + 1))) / (1 - a) ; :: thesis: S1[n + 1]
hence () . (n + 1) = ((1 - (a |^ (n + 1))) / (1 - a)) + (s . (n + 1)) by SERIES_1:def 1
.= ((1 - (a |^ (n + 1))) / (1 - a)) + ((a |^ (n + 1)) * 1) by A2
.= ((1 - (a |^ (n + 1))) / (1 - a)) + ((a |^ (n + 1)) * ((1 - a) / (1 - a))) by
.= ((1 - (a |^ (n + 1))) / (1 - a)) + (((a |^ (n + 1)) * (1 - a)) / (1 - a)) by XCMPLX_1:74
.= ((1 - (a |^ (n + 1))) + ((a |^ (n + 1)) - ((a |^ (n + 1)) * a))) / (1 - a) by XCMPLX_1:62
.= ((1 - (a |^ (n + 1))) + ((a |^ (n + 1)) - (a |^ ((n + 1) + 1)))) / (1 - a) by NEWTON:6
.= (1 - (a |^ ((n + 1) + 1))) / (1 - a) ;
:: thesis: verum
end;
() . 0 = s . 0 by SERIES_1:def 1
.= a |^ 0 by A2
.= 1 by NEWTON:4
.= (1 - a) / (1 - a) by
.= (1 - (a |^ (0 + 1))) / (1 - a) ;
then A4: S1[ 0 ] ;
for n being Nat holds S1[n] from NAT_1:sch 2(A4, A3);
hence (Partial_Sums s) . n = (1 - (a |^ (n + 1))) / (1 - a) ; :: thesis: verum