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