theorem Th14: :: NEWTON02:112

for f, F being FinSequence of REAL holds Sum (f ^ F) = (Sum f) + (Sum F)