for f being Real_Sequence holds f ^ f is real-valued Complex_Sequence ;