theorem Th43: :: SIN_COS:44

for th being Real holds th rExpSeq = Re (th ExpSeq)