let s be Real_Sequence; :: thesis: ( ( for n being Nat st n >= 1 holds
( s . n = 1 / ((n - 1) * (n + 1)) & s . 0 = 0 ) ) implies for n being Nat st n >= 2 holds
(Partial_Sums s) . n = ((3 / 4) - (1 / (2 * n))) - (1 / (2 * (n + 1))) )
defpred S₁[ Nat] means (Partial_Sums s) . $1 = ((3 / 4) - (1 / (2 * $1))) - (1 / (2 * ($1 + 1)));
assume A1: for n being Nat st n >= 1 holds
( s . n = 1 / ((n - 1) * (n + 1)) & s . 0 = 0 ) ; :: thesis: for n being Nat st n >= 2 holds
(Partial_Sums s) . n = ((3 / 4) - (1 / (2 * n))) - (1 / (2 * (n + 1)))
then A2: s . 1 = 1 / ((1 - 1) * (1 + 1))
.= 0 by XCMPLX_1:49 ;
A3: for n being Nat st n >= 2 & S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( n >= 2 & S₁[n] implies S₁[n + 1] )
assume that
A4: n >= 2 and
A5: (Partial_Sums s) . n = ((3 / 4) - (1 / (2 * n))) - (1 / (2 * (n + 1))) ; :: thesis: S₁[n + 1]
A6: n > 0 by A4, XXREAL_0:2;
then A7: n + 1 > 1 by XREAL_1:29;
A8: n + 2 >= n by NAT_1:11;
(Partial_Sums s) . (n + 1) = (((3 / 4) - (1 / (2 * n))) - (1 / (2 * (n + 1)))) + (s . (n + 1)) by A5, SERIES_1:def 1
.= (((3 / 4) - (1 / (2 * n))) - (1 / (2 * (n + 1)))) + (1 / (((n + 1) - 1) * ((n + 1) + 1))) by A1, A7
.= ((3 / 4) - (1 / (2 * (n + 1)))) + ((1 / (n * (n + 2))) - (1 / (2 * n)))
.= ((3 / 4) - (1 / (2 * (n + 1)))) + ((1 / (n * (n + 2))) - ((1 / 2) * (1 / n))) by XCMPLX_1:102
.= ((3 / 4) - (1 / (2 * (n + 1)))) + (((1 / n) * (1 / (n + 2))) - ((1 / 2) * (1 / n))) by XCMPLX_1:102
.= ((3 / 4) - (1 / (2 * (n + 1)))) + (((1 / (n + 2)) - (1 / 2)) * (1 / n))
.= ((3 / 4) - (1 / (2 * (n + 1)))) + ((((1 * 2) - (1 * (n + 2))) / ((n + 2) * 2)) * (1 / n)) by A6, A8, XCMPLX_1:130
.= ((3 / 4) - (1 / (2 * (n + 1)))) + (((- n) / n) * (1 / ((n + 2) * 2))) by XCMPLX_1:85
.= ((3 / 4) - (1 / (2 * (n + 1)))) + ((- 1) * (1 / ((n + 2) * 2))) by A6, XCMPLX_1:197
.= ((3 / 4) - (1 / (2 * (n + 1)))) + (- (1 / (2 * ((n + 1) + 1)))) ;
hence S₁[n + 1] ; :: thesis: verum

end;

(Partial_Sums s) . (1 + 1) = ((Partial_Sums s) . (1 + 0)) + (s . 2) by SERIES_1:def 1
.= (((Partial_Sums s) . 0) + (s . 1)) + (s . 2) by SERIES_1:def 1
.= ((s . 0) + (s . 1)) + (s . 2) by SERIES_1:def 1
.= (0 + (s . 1)) + (s . 2) by A1
.= 1 / ((2 - 1) * (2 + 1)) by A1, A2
.= ((3 / 4) - (1 / (2 * 2))) - (1 / (2 * (2 + 1))) ;
then A9: S₁[2] ;
for n being Nat st n >= 2 holds
S₁[n] from NAT_1:sch 8(A9, A3);
hence for n being Nat st n >= 2 holds
(Partial_Sums s) . n = ((3 / 4) - (1 / (2 * n))) - (1 / (2 * (n + 1))) ; :: thesis: verum