theorem Th7: :: MAZURULM:7

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