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