theorem Th9: :: MAZURULM:9

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