let F, F1, F2 be FinSequence of REAL ; :: thesis: for r1, r2 being Real st ( F1 = <*r1*> ^ F or F1 = F ^ <*r1*> ) & ( F2 = <*r2*> ^ F or F2 = F ^ <*r2*> ) holds
Sum (F1 - F2) = r1 - r2
let r1, r2 be Real; :: thesis: ( ( F1 = <*r1*> ^ F or F1 = F ^ <*r1*> ) & ( F2 = <*r2*> ^ F or F2 = F ^ <*r2*> ) implies Sum (F1 - F2) = r1 - r2 )
assume that
A1: ( F1 = <*r1*> ^ F or F1 = F ^ <*r1*> ) and
A2: ( F2 = <*r2*> ^ F or F2 = F ^ <*r2*> ) ; :: thesis: Sum (F1 - F2) = r1 - r2
len F1 = (len F) + (len <*r1*>) by A1, FINSEQ_1:22;
then A3: len F1 = (len F) + 1 by FINSEQ_1:39;
len F2 = (len <*r2*>) + (len F) by A2, FINSEQ_1:22;
then A4: len F2 = 1 + (len F) by FINSEQ_1:39;
F1 - F2 = diffreal .: (F1,F2) by RVSUM_1:def 6;
then A5: len F1 = len (F1 - F2) by A3, A4, FINSEQ_2:72;
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 A7: F1 . k = F1 /. k by PARTFUN1:def 6;
A8: k in Seg (len F1) by A6, FINSEQ_1:def 3;
then k in dom F2 by A3, A4, FINSEQ_1:def 3;
then A9: F2 . k = F2 /. k by PARTFUN1:def 6;
k in dom (F1 - F2) by A5, A8, FINSEQ_1:def 3;
hence (F1 - F2) . k = (F1 /. k) - (F2 /. k) by A7, A9, VALUED_1:13; :: thesis: verum

end;

then A10: Sum (F1 - F2) = (Sum F1) - (Sum F2) by A3, A4, A5, INTEGRA1:22;
( Sum F1 = r1 + (Sum F) & Sum F2 = (Sum F) + r2 ) by A1, A2, RVSUM_1:74, RVSUM_1:76;
hence Sum (F1 - F2) = r1 - r2 by A10; :: thesis: verum