let F1, F2 be FinSequence of REAL ; :: thesis: ( len F1 = len F2 implies ( len (F1 + F2) = len F1 & len (F1 - F2) = len F1 & Sum (F1 + F2) = (Sum F1) + (Sum F2) & Sum (F1 - F2) = (Sum F1) - (Sum F2) ) )
assume A1: len F1 = len F2 ; :: thesis: ( len (F1 + F2) = len F1 & len (F1 - F2) = len F1 & Sum (F1 + F2) = (Sum F1) + (Sum F2) & Sum (F1 - F2) = (Sum F1) - (Sum F2) )
F1 + F2 = addreal .: (F1,F2) by RVSUM_1:def 4;
hence A2: len F1 = len (F1 + F2) by A1, FINSEQ_2:72; :: thesis: ( len (F1 - F2) = len F1 & Sum (F1 + F2) = (Sum F1) + (Sum F2) & Sum (F1 - F2) = (Sum F1) - (Sum F2) )
F1 - F2 = diffreal .: (F1,F2) by RVSUM_1:def 6;
hence A3: len F1 = len (F1 - F2) by A1, FINSEQ_2:72; :: thesis: ( Sum (F1 + F2) = (Sum F1) + (Sum F2) & Sum (F1 - F2) = (Sum F1) - (Sum F2) )
for k being Element of NAT st k in dom F1 holds
(F1 + F2) . k = (F1 /. k) + (F2 /. k)

proof

let k be Element of NAT ; :: thesis: ( k in dom F1 implies (F1 + F2) . k = (F1 /. k) + (F2 /. k) )
assume A4: k in dom F1 ; :: thesis: (F1 + F2) . k = (F1 /. k) + (F2 /. k)
then A5: F1 . k = F1 /. k by PARTFUN1:def 6;
A6: k in Seg (len F1) by A4, FINSEQ_1:def 3;
then k in dom F2 by A1, FINSEQ_1:def 3;
then A7: F2 . k = F2 /. k by PARTFUN1:def 6;
k in dom (F1 + F2) by A2, A6, FINSEQ_1:def 3;
hence (F1 + F2) . k = (F1 /. k) + (F2 /. k) by A5, A7, VALUED_1:def 1; :: thesis: verum

end;

hence Sum (F1 + F2) = (Sum F1) + (Sum F2) by A1, A2, INTEGRA1:21; :: thesis: Sum (F1 - F2) = (Sum F1) - (Sum F2)
for k being Element of NAT st k in dom F1 holds
(F1 - F2) . k = (F1 /. k) - (F2 /. k)

proof

let k be Element of NAT ; :: thesis: ( k in dom F1 implies (F1 - F2) . k = (F1 /. k) - (F2 /. k) )
assume A8: k in dom F1 ; :: thesis: (F1 - F2) . k = (F1 /. k) - (F2 /. k)
then A9: F1 . k = F1 /. k by PARTFUN1:def 6;
A10: k in Seg (len F1) by A8, FINSEQ_1:def 3;
then k in dom F2 by A1, FINSEQ_1:def 3;
then A11: F2 . k = F2 /. k by PARTFUN1:def 6;
k in dom (F1 - F2) by A3, A10, FINSEQ_1:def 3;
hence (F1 - F2) . k = (F1 /. k) - (F2 /. k) by A9, A11, VALUED_1:13; :: thesis: verum

end;

hence Sum (F1 - F2) = (Sum F1) - (Sum F2) by A1, A3, INTEGRA1:22; :: thesis: verum