theorem :: RVSUM_4:20

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