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

now :: thesis: for n1, n2 being Nat st m <= n1 & m <= n2 holds
|.((dblseq_ex_1 . (n1,n2)) - 0).| < 1 / m

let n1, n2 be Nat; :: thesis: ( m <= n1 & m <= n2 implies |.((dblseq_ex_1 . (n1,n2)) - 0).| < 1 / m )
assume that
A1: m <= n1 and
m <= n2 ; :: thesis: |.((dblseq_ex_1 . (n1,n2)) - 0).| < 1 / m
m + 0 < n1 + 1 by A1, XREAL_1:8;
then 1 / (n1 + 1) < 1 / m by XREAL_1:76;
then |.((1 / (n1 + 1)) - 0).| < 1 / m by ABSVALUE:def 1;
hence |.((dblseq_ex_1 . (n1,n2)) - 0).| < 1 / m by Def5; :: thesis: verum

end;

hence ex n being Nat st
for n1, n2 being Nat st n <= n1 & n <= n2 holds
|.((dblseq_ex_1 . (n1,n2)) - 0).| < 1 / m ; :: thesis: verum