for m being non zero Nat ex n being Nat st
for n1, n2 being Nat st n <= n1 & n <= n2 holds
|.((dblseq_ex_1 . (n1,n2)) - 0).| < 1 / m