theorem Th20: :: NDIFF_1:20

for S being RealNormSpace
for seq being sequence of S
for x0 being Point of S
for r being Real st 0 < r & ( for n being Nat holds seq . n = (1 / (n + r)) * x0 ) holds
lim seq = 0. S