theorem Th46: :: FLEXARY1:46

for f, g being FinSequence-yielding complex-functions-valued FinSequence holds Sum (f ^ g) = (Sum f) ^ (Sum g)