theorem Th45: :: SIN_COS:46

for p, q being Real holds Sum ((p + q) rExpSeq) = (Sum (p rExpSeq)) * (Sum (q rExpSeq))