let a be Real; :: thesis: for s being Real_Sequence st a <> 1 & ( for n being Nat st n >= 1 holds

( s . n = (a / (a - 1)) |^ n & s . 0 = 0 ) ) holds

for n being Nat st n >= 1 holds

(Partial_Sums s) . n = a * (((a / (a - 1)) |^ n) - 1)

let s be Real_Sequence; :: thesis: ( a <> 1 & ( for n being Nat st n >= 1 holds

( s . n = (a / (a - 1)) |^ n & s . 0 = 0 ) ) implies for n being Nat st n >= 1 holds

(Partial_Sums s) . n = a * (((a / (a - 1)) |^ n) - 1) )

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

assume a <> 1 ; :: thesis: ( ex n being Nat st

( n >= 1 & not ( s . n = (a / (a - 1)) |^ n & s . 0 = 0 ) ) or for n being Nat st n >= 1 holds

(Partial_Sums s) . n = a * (((a / (a - 1)) |^ n) - 1) )

then A1: a - 1 <> 0 ;

assume A2: for n being Nat st n >= 1 holds

( s . n = (a / (a - 1)) |^ n & s . 0 = 0 ) ; :: thesis: for n being Nat st n >= 1 holds

(Partial_Sums s) . n = a * (((a / (a - 1)) |^ n) - 1)

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

S_{1}[n + 1]

.= (s . 0) + (s . 1) by SERIES_1:def 1

.= 0 + (s . 1) by A2

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

.= ((a / (a - 1)) + a) - a

.= ((a * (1 / (a - 1))) + (a * 1)) - a by XCMPLX_1:99

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

.= (a * ((1 / (a - 1)) + ((a - 1) / (a - 1)))) - a

.= (a * ((1 + (a - 1)) / (a - 1))) - a by XCMPLX_1:62

.= a * ((a / (a - 1)) - 1)

.= a * (((a / (a - 1)) |^ 1) - 1) ;

then A6: S_{1}[1]
;

for n being Nat st n >= 1 holds

S_{1}[n]
from NAT_1:sch 8(A6, A3);

hence for n being Nat st n >= 1 holds

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

( s . n = (a / (a - 1)) |^ n & s . 0 = 0 ) ) holds

for n being Nat st n >= 1 holds

(Partial_Sums s) . n = a * (((a / (a - 1)) |^ n) - 1)

let s be Real_Sequence; :: thesis: ( a <> 1 & ( for n being Nat st n >= 1 holds

( s . n = (a / (a - 1)) |^ n & s . 0 = 0 ) ) implies for n being Nat st n >= 1 holds

(Partial_Sums s) . n = a * (((a / (a - 1)) |^ n) - 1) )

defpred S

assume a <> 1 ; :: thesis: ( ex n being Nat st

( n >= 1 & not ( s . n = (a / (a - 1)) |^ n & s . 0 = 0 ) ) or for n being Nat st n >= 1 holds

(Partial_Sums s) . n = a * (((a / (a - 1)) |^ n) - 1) )

then A1: a - 1 <> 0 ;

assume A2: for n being Nat st n >= 1 holds

( s . n = (a / (a - 1)) |^ n & s . 0 = 0 ) ; :: thesis: for n being Nat st n >= 1 holds

(Partial_Sums s) . n = a * (((a / (a - 1)) |^ n) - 1)

A3: for n being Nat st n >= 1 & S

S

proof

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

assume that

n >= 1 and

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

A5: n + 1 >= 1 by NAT_1:11;

(Partial_Sums s) . (n + 1) = (a * (((a / (a - 1)) |^ n) - 1)) + (s . (n + 1)) by A4, SERIES_1:def 1

.= ((a * ((a / (a - 1)) |^ n)) - a) + ((a / (a - 1)) |^ (n + 1)) by A2, A5

.= ((a * ((a / (a - 1)) |^ n)) + ((a / (a - 1)) |^ (n + 1))) - a

.= ((a * ((a / (a - 1)) |^ n)) + (((a / (a - 1)) |^ n) * (a / (a - 1)))) - a by NEWTON:6

.= (((a / (a - 1)) |^ n) * ((a * 1) + (a / (a - 1)))) - a

.= (((a / (a - 1)) |^ n) * ((a * 1) + (a * (1 / (a - 1))))) - a by XCMPLX_1:99

.= (((a / (a - 1)) |^ n) * (a * (1 + (1 / (a - 1))))) - a

.= (((a / (a - 1)) |^ n) * (a * (((a - 1) / (a - 1)) + (1 / (a - 1))))) - a by A1, XCMPLX_1:60

.= (((a / (a - 1)) |^ n) * (a * (((a - 1) + 1) / (a - 1)))) - a by XCMPLX_1:62

.= (a * (((a / (a - 1)) |^ n) * (a / (a - 1)))) - a

.= (a * ((a / (a - 1)) |^ (n + 1))) - a by NEWTON:6

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

hence S_{1}[n + 1]
; :: thesis: verum

end;assume that

n >= 1 and

A4: (Partial_Sums s) . n = a * (((a / (a - 1)) |^ n) - 1) ; :: thesis: S

A5: n + 1 >= 1 by NAT_1:11;

(Partial_Sums s) . (n + 1) = (a * (((a / (a - 1)) |^ n) - 1)) + (s . (n + 1)) by A4, SERIES_1:def 1

.= ((a * ((a / (a - 1)) |^ n)) - a) + ((a / (a - 1)) |^ (n + 1)) by A2, A5

.= ((a * ((a / (a - 1)) |^ n)) + ((a / (a - 1)) |^ (n + 1))) - a

.= ((a * ((a / (a - 1)) |^ n)) + (((a / (a - 1)) |^ n) * (a / (a - 1)))) - a by NEWTON:6

.= (((a / (a - 1)) |^ n) * ((a * 1) + (a / (a - 1)))) - a

.= (((a / (a - 1)) |^ n) * ((a * 1) + (a * (1 / (a - 1))))) - a by XCMPLX_1:99

.= (((a / (a - 1)) |^ n) * (a * (1 + (1 / (a - 1))))) - a

.= (((a / (a - 1)) |^ n) * (a * (((a - 1) / (a - 1)) + (1 / (a - 1))))) - a by A1, XCMPLX_1:60

.= (((a / (a - 1)) |^ n) * (a * (((a - 1) + 1) / (a - 1)))) - a by XCMPLX_1:62

.= (a * (((a / (a - 1)) |^ n) * (a / (a - 1)))) - a

.= (a * ((a / (a - 1)) |^ (n + 1))) - a by NEWTON:6

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

hence S

.= (s . 0) + (s . 1) by SERIES_1:def 1

.= 0 + (s . 1) by A2

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

.= ((a / (a - 1)) + a) - a

.= ((a * (1 / (a - 1))) + (a * 1)) - a by XCMPLX_1:99

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

.= (a * ((1 / (a - 1)) + ((a - 1) / (a - 1)))) - a

.= (a * ((1 + (a - 1)) / (a - 1))) - a by XCMPLX_1:62

.= a * ((a / (a - 1)) - 1)

.= a * (((a / (a - 1)) |^ 1) - 1) ;

then A6: S

for n being Nat st n >= 1 holds

S

hence for n being Nat st n >= 1 holds

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