theorem Th41: :: SIN_COS:42
for p being Real holds Im (Sum (p ExpSeq)) = 0