let r be Real; :: thesis: for seq being Real_Sequence st 0 <= r & ( for n being Nat holds seq . n = 1 / ((n * n) + r) ) holds
lim seq = 0
let seq be Real_Sequence; :: thesis: ( 0 <= r & ( for n being Nat holds seq . n = 1 / ((n * n) + r) ) implies lim seq = 0 )
assume that
A1: 0 <= r and
A2: for n being Nat holds seq . n = 1 / ((n * n) + r) ; :: thesis: lim seq = 0
A3: seq is convergent by A1, A2, Th32;
for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - 0).| < p by A1, A2, LmTh32;
hence lim seq = 0 by A3, SEQ_2:def 7; :: thesis: verum