theorem Th2: :: INTEGRA5:2

for F1, F2 being FinSequence of REAL st len F1 = len F2 holds
( len (F1 + F2) = len F1 & len (F1 - F2) = len F1 & Sum (F1 + F2) = (Sum F1) + (Sum F2) & Sum (F1 - F2) = (Sum F1) - (Sum F2) )