for r being Element of REAL holds P-lim ([:NAT,NAT:] --> r) = r