theorem Th41: :: SIN_COS:42

for p being Real holds Im (Sum (p ExpSeq)) = 0