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

for n1, n2 being Nat st n <= n1 & n <= n2 holds

|.((dblseq_ex_1 . (n1,n2)) - 0).| < 1 / m ; :: thesis: verum

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

hence
ex n being Nat st |.((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;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

for n1, n2 being Nat st n <= n1 & n <= n2 holds

|.((dblseq_ex_1 . (n1,n2)) - 0).| < 1 / m ; :: thesis: verum