:: deftheorem defines ^ RVSUM_4:def 5 :
for seq being Complex_Sequence
for f being Function holds seq ^ f = seq;