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

(Partial_Sums s) . 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

(Partial_Sums s) . 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 (Partial_Sums s) . n = (1 - (a |^ (n + 1))) / (1 - a) )

defpred S_{1}[ Nat] means (Partial_Sums s) . $1 = (1 - (a |^ ($1 + 1))) / (1 - a);

assume a <> 1 ; :: thesis: ( ex n being Nat st not s . n = a |^ n or (Partial_Sums s) . n = (1 - (a |^ (n + 1))) / (1 - a) )

then A1: 1 - a <> 0 ;

assume A2: for n being Nat holds s . n = a |^ n ; :: thesis: (Partial_Sums s) . n = (1 - (a |^ (n + 1))) / (1 - a)

A3: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]

.= a |^ 0 by A2

.= 1 by NEWTON:4

.= (1 - a) / (1 - a) by A1, XCMPLX_1:60

.= (1 - (a |^ (0 + 1))) / (1 - a) ;

then A4: S_{1}[ 0 ]
;

for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A4, A3);

hence (Partial_Sums s) . n = (1 - (a |^ (n + 1))) / (1 - a) ; :: thesis: verum

for s being Real_Sequence st a <> 1 & ( for n being Nat holds s . n = a |^ n ) holds

(Partial_Sums s) . 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

(Partial_Sums s) . 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 (Partial_Sums s) . n = (1 - (a |^ (n + 1))) / (1 - a) )

defpred S

assume a <> 1 ; :: thesis: ( ex n being Nat st not s . n = a |^ n or (Partial_Sums s) . n = (1 - (a |^ (n + 1))) / (1 - a) )

then A1: 1 - a <> 0 ;

assume A2: for n being Nat holds s . n = a |^ n ; :: thesis: (Partial_Sums s) . n = (1 - (a |^ (n + 1))) / (1 - a)

A3: for n being Nat st S

S

proof

(Partial_Sums s) . 0 =
s . 0
by SERIES_1:def 1
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume (Partial_Sums s) . n = (1 - (a |^ (n + 1))) / (1 - a) ; :: thesis: S_{1}[n + 1]

hence (Partial_Sums s) . (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 A1, XCMPLX_1:60

.= ((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;assume (Partial_Sums s) . n = (1 - (a |^ (n + 1))) / (1 - a) ; :: thesis: S

hence (Partial_Sums s) . (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 A1, XCMPLX_1:60

.= ((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

.= a |^ 0 by A2

.= 1 by NEWTON:4

.= (1 - a) / (1 - a) by A1, XCMPLX_1:60

.= (1 - (a |^ (0 + 1))) / (1 - a) ;

then A4: S

for n being Nat holds S

hence (Partial_Sums s) . n = (1 - (a |^ (n + 1))) / (1 - a) ; :: thesis: verum