theorem Th44: :: MATRIXC1:46

for F1, F2 being FinSequence of COMPLEX holds Sum (F1 ^ F2) = (Sum F1) + (Sum F2)