for t being Real
for f being convergent Real_Sequence holds lim (t + f) = t + (lim f)