let X be non empty set ; :: thesis: 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); :: thesis: ( len F >= 2 implies (Partial_Sums F) /. 2 = (F /. 1) + (F /. 2) )
assume A1: len F >= 2 ; :: thesis: (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; :: thesis: verum