theorem Th47: :: SIN_COS:48

for th being Real holds exp_R . th = Re (Sum (th ExpSeq))