theorem Th44: :: SIN_COS:45

for th being Real holds
( th rExpSeq is summable & Sum (th rExpSeq) = Re (Sum (th ExpSeq)) )