let s be Real_Sequence; :: thesis: ( ( for n being Element of NAT holds s . n = 1 / ((n * (n + 1)) * (n + 2)) ) implies for n being Element of NAT holds (Partial_Sums s) . n = (1 / 4) - (1 / ((2 * (n + 1)) * (n + 2))) )
assume A1:
for n being Element of NAT holds s . n = 1 / ((n * (n + 1)) * (n + 2))
; :: thesis: for n being Element of NAT holds (Partial_Sums s) . n = (1 / 4) - (1 / ((2 * (n + 1)) * (n + 2)))
defpred S1[ Element of NAT ] means (Partial_Sums s) . $1 = (1 / 4) - (1 / ((2 * ($1 + 1)) * ($1 + 2)));
(Partial_Sums s) . 0 =
s . 0
by SERIES_1:def 1
.=
1 / ((0 * (0 + 1)) * (0 + 2))
by A1
.=
(1 / 4) - (1 / ((2 * (0 + 1)) * (0 + 2)))
by XCMPLX_1:49
;
then A2:
S1[ 0 ]
;
A3:
for n being Element of NAT st S1[n] holds
S1[n + 1]
for n being Element of NAT holds S1[n]
from NAT_1:sch 1(A2, A3);
hence
for n being Element of NAT holds (Partial_Sums s) . n = (1 / 4) - (1 / ((2 * (n + 1)) * (n + 2)))
; :: thesis: verum