theorem :: RVSUM_4:18

for rseq being Real_Sequence holds (<%> REAL) ^ rseq is real-valued Complex_Sequence ;