theorem Th44: :: SIN_COS:45
for th being Real holds
( th rExpSeq is summable & Sum (th rExpSeq) = Re (Sum (th ExpSeq)) )