theorem Th1: :: INTEGRA5:1

for F, F1, F2 being FinSequence of REAL
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