theorem Th21: :: RFUNCT_3:21

for D being non empty set
for f1, f2 being FinSequence of PFuncs (D,REAL) holds Sum (f1 ^ f2) = (Sum f1) + (Sum f2)