for t being Real
for f being Real_Sequence holds f + (NAT --> t) = t + f