theorem Th6: :: MAZURULM:6

for r being Element of REAL holds lim (NAT --> r) = r