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