let X be non empty set ; for F being summable FinSequence of Funcs (X,ExtREAL) st len F >= 2 holds
(Partial_Sums F) /. 2 = (F /. 1) + (F /. 2)
let F be summable FinSequence of Funcs (X,ExtREAL); ( len F >= 2 implies (Partial_Sums F) /. 2 = (F /. 1) + (F /. 2) )
assume A1:
len F >= 2
; (Partial_Sums F) /. 2 = (F /. 1) + (F /. 2)
then
1 + 1 <= len F
;
then A3:
1 < len F
by NAT_1:13;
then A6:
( 1 in dom F & 2 in dom F )
by A1, FINSEQ_3:25;
len F = len (Partial_Sums F)
by MEASUR11:def 11;
then A5:
( 1 in dom (Partial_Sums F) & 2 in dom (Partial_Sums F) )
by A1, A3, FINSEQ_3:25;
then A4: (Partial_Sums F) /. 1 =
(Partial_Sums F) . 1
by PARTFUN1:def 6
.=
F . 1
by MEASUR11:def 11
.=
F /. 1
by A6, PARTFUN1:def 6
;
(Partial_Sums F) . (1 + 1) = ((Partial_Sums F) /. 1) + (F /. (1 + 1))
by A1, NAT_1:13, MEASUR11:def 11;
hence
(Partial_Sums F) /. 2 = (F /. 1) + (F /. 2)
by A4, A5, PARTFUN1:def 6; verum