:: deftheorem defines ^ RVSUM_4:def 7 :
for f being Real_Sequence
for g being Function holds f ^ g = f;