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:86; :: 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:86; :: 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 k in Seg (len F1) by FINSEQ_1:def 3;
then A5: ( k in dom (F1 + F2) & k in dom F2 ) by A1, A2, FINSEQ_1:def 3;
then ( F1 . k = F1 /. k & F2 . k = F2 /. k ) by A4, PARTFUN1:def 8;
hence (F1 + F2) . k = (F1 /. k) + (F2 /. k) by A5, VALUED_1:def 1; :: thesis: verum
end;
hence Sum (F1 + F2) = (Sum F1) + (Sum F2) by A1, A2, INTEGRA1:23; :: 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 A6: k in dom F1 ; :: thesis: (F1 - F2) . k = (F1 /. k) - (F2 /. k)
then k in Seg (len F1) by FINSEQ_1:def 3;
then A7: ( k in dom (F1 - F2) & k in dom F2 ) by A1, A3, FINSEQ_1:def 3;
then ( F1 . k = F1 /. k & F2 . k = F2 /. k ) by A6, PARTFUN1:def 8;
hence (F1 - F2) . k = (F1 /. k) - (F2 /. k) by A7, VALUED_1:13; :: thesis: verum
end;
hence Sum (F1 - F2) = (Sum F1) - (Sum F2) by A1, A3, INTEGRA1:24; :: thesis: verum