for E being RealNormSpace
for a being Point of E holds lim (NAT --> a) = a