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₁[ 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₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( n >= 1 & S₁[n] implies S₁[n + 1] )
assume that
n >= 1 and
A4: (Partial_Sums s) . n = a * (((a / (a - 1)) |^ n) - 1) ; :: thesis: S₁[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₁[n + 1] ; :: thesis: verum

end;

(Partial_Sums s) . (0 + 1) = ((Partial_Sums s) . 0) + (s . (0 + 1)) by SERIES_1:def 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] ;
for n being Nat st n >= 1 holds
S₁[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