theorem Th33: :: SEQ_4:33

for r being Real
for seq being Real_Sequence st 0 <= r & ( for n being Nat holds seq . n = 1 / ((n * n) + r) ) holds
lim seq = 0