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