theorem Th5: :: MAZURULM:5

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