Precise proof of equivalence of two definitions of limit of a function Consider two (equivalent) definitions of a (real) limit of a function $f:\mathbb{R}\rightarrow\mathbb{R}$.
The epsilon-delta one:
$$
\lim_{x\to x_0} f(x)=l \iff \forall \varepsilon>0\exists \delta>0\forall x\in D_f: (0<|x-x_0|<\delta \Rightarrow |f(x)-l|<\varepsilon)
$$
and the sequential one:
$$
\lim_{x\to x_0} f(x)=l \iff \forall(x_n)\subseteq (D_f\setminus\{x_0\}):(\lim_{n\to\infty}x_n=x_0 \Rightarrow \lim_{n\to\infty}f(x_n)=l)
$$
where $(x_n)\subseteq (D_f\setminus\{x_0\})$ stands for a number sequence that takes values only from the domain of $f$ without $x_0$.
I have spent hours trying to come up with or to find an axiomatic proof of their equivalence. I have seen a few different proofs, but they all seem to be imprecise, at some point just "stating the obvious".
So, is there a book, an article, a site, a lecture or something, where I can get (maybe long and boring, but still) a formal proof of this fact? Or maybe precise proofs for this fact need more advanced theory, which is not even in my books yet? Maybe I need a better understanding of what is "precise"?
 A: Here is my own proof. Please tell me what if any steps of this seem "imprecise" to you.
If $f$ has an "epsilon-delta limit" of $l$ at $x_0$, then $f$ has a "sequence limit" of $l$ at $x_0$: Let $(x_n)$ be a sequence in $D_f\setminus\{x_0\}$ such that $\displaystyle\lim_{n \to \infty} x_n=x_0$. We need to show that $\displaystyle\lim_{n \to \infty} f(x_n)=l$. Let $\epsilon>0$. Then, since $f$ has an "epsilon-delta limit" of $l$ at $x_0$, there exists $\delta>0$ such that for all $x \in D_f$ satisfying $0 <|x-x_0|<\delta$, we have $|f(x)-l|<\epsilon$. Since $\displaystyle\lim_{n \to \infty}x_n=x_0$, there exists $N \in \mathbb{N}$ such that for all $n \geq N$, $|x_n-x_0|<\delta$. Then $0<|x_n-x_0|<\delta$ for all $n \geq N$, so $|f(x_n)-\ell|<\epsilon$ for all $n \geq N$. We have shown that given $\epsilon>0$, there exists $N \in \mathbb{N}$ such that for all $n \geq N$, $|f(x_n)-l|<\epsilon$. Thus $\displaystyle\lim_{n \to \infty}f(x_n)=l$.
If $f$ has a "sequence limit" of $l$ at $x_0$, then $f$ has an "epsilon-delta limit" of $l$ at $x_0$: We will prove the contrapositive, i.e., if $f$ does not have an "epsilon-delta limit" of $l$ at $x_0$, then $f$ does not have a "sequence limit" of $l$ at $x_0$. If $f$ does not have an "epsilon-delta" limit of $l$ at $x_0$, then there exists $\epsilon>0$ such that for all $\delta>0$, there exists $x \in D_f$ satisfying $0<|x-x_0|<\delta$, and yet $|f(x)-l| \geq \epsilon$. To show that $f$ does not have a "sequence limit" of $l$ at $x_0$, we must exhibit a sequence $(x_n)\in D_f \setminus\{x_0\}$ such that $\displaystyle\lim_{n \to \infty}x_n=x_0$ and yet $\displaystyle\lim_{n \to \infty}f(x_n) \neq l$. 
We construct the sequence as follows. Setting $\delta_1=1$, there exists $x_1\in D_f$ with $0<|x_1-x_0|<\delta_1=1$ such that $|f(x_1)-l| \geq \epsilon$. (Note then that $x_1 \neq x_0$, so in fact $x_1 \in D_f \setminus\{x_0\}$.) Similarly, setting $\delta_2=\frac{1}{2}$, there exists $x_2 \in D_f$ with $0<|x_2-x_0|<\delta_2=\frac{1}{2}$ such that $|f(x_2)-l| \geq \epsilon$. (Once again, $x_2 \neq x_0$, so $x_2 \in D_f \setminus\{x_0\}$.) Now suppose we have chosen $x_1,x_2,\dots,x_n \in D_f \setminus\{x_0\}$ such that $|x_i-x_0|<\frac{1}{i}$ and $|f(x_i)-l| \geq \epsilon$ for all $1 \leq i \leq n$. Setting $\delta_{n+1}=\frac{1}{n+1}$, there exists $x_{n+1} \in D_f$ with $0 \leq |x_{n+1}-x_0|<\frac{1}{n+1}$ such that $|f(x_{n+1})-l| \geq \epsilon$, so we let $x_{n+1}$ be the next term of the sequence. By the axiom of dependent choice, we can define a sequence $(x_n) \in D_f \setminus\{x_0\}$ such that $0<|x_i-x_0|<\frac{1}{i}$ but $|f(x_i)-l| \geq \epsilon$ for all $i \geq 1$. 
Claim: $\displaystyle\lim_{n \to \infty} x_n=x_0$. Let $\eta>0$. Then there exists a natural number $N>\frac{1}{\eta}$. For all $n \geq N$, $|x_n-x_0|<\frac{1}{n}\leq\frac{1}{N}< \frac{1}{1/\eta}=\eta$. So $\displaystyle\lim_{n \to \infty} x_n=x_0$.
Claim: $\displaystyle\lim_{n \to \infty} f(x_n)=x_0$. Let $\epsilon$ be as above. Choose any $M \in \mathbb{N}$. Then for any $m \geq M$, $|f(x_m)-l| \geq \epsilon$. (Note: this is stronger than we need. We only need to show there exists $m \geq M$ satisfying that equation.) Hence $\displaystyle\lim_{n \to \infty} f(x_n) \neq l$.

It is good to be careful when one is first learning to write proofs, but as we can see above, sometimes including all the details makes proofs long and tedious. For instance, if I were writing this proof elsewhere, I would said that it is clear that the sequence $(x_n)$ satisfying $|x_i-x_0|<\frac{1}{i}$ for all $i$ converges to $x_0$. I would have also said it's clear that $\displaystyle\lim_{n \to \infty} f(x_n) \neq l$ is clear if each term $f(x_i)$ satisfies $|f(x_i)-l| \geq \epsilon$. And when defining that sequence $(x_n)$ inductively, I might not have written out the whole induction argument, but rather said "and so on..." These sorts of shortcuts are not necessarily imprecise. They are just an indicator that the fact that is claimed is routine to verify, and so the author has not taken the time and space to spell out all the details.
A: Call the epsilon-delta def'n "$I$" and the sequential def'n "$II$".
To show  $I\implies II:$ Let $(x_n)_n$ be any sequence in $D_f$ converging to $x.$ For any $e >0,$ take $d_e >0$ such that $$ (\bullet ) \;\forall y\in D_f\cap (-d_e+x,d_e +x)\; ( |f(y)-l|<e).$$  Now $\lim_{n\to \infty}x_n=x$ implies that $\{n: x_n\not \in (-d_e+x,d_e+x)\}$ is finite, so    $$\exists m_e\;\forall n\geq m_e\; (x_n\in D_f\cap (-d_e+x,d_e+x)\;).$$ Applying $(\bullet )$ to this we have $$\exists m_e\; \forall n\geq m_e\; (|f(x_n)-l|<e).$$ This holds for any $e>0,$ so $(f(x_n))_n$ converges to $l.$
To show  $(\neg I) \implies (\neg II):$ The negation of $I$ is $$\exists e>0\;\forall d>0\;\exists y\in D_f\cap (-d+x,d+x)\;(|f(y)-l|\geq e.$$  Take such an $e.$ For each $n\in \mathbb N$ let $d_n=2^{-n}$ and take $x_n\in D_f\cap (-d_n+x,d_n+x)$ such that $|f(x_n)-l|\geq e.$ Then $(x_n)_n$ is a sequence in $D_f$ converging to $x,$ and $(f(x_n))_n$ does not converge to $l,$ so we have $(\neg II).$
A: I cannot add comments. What is unclear? The definition of limit of a sequence? If so, see below:
We have (from the definition of limit of a sequence) that
$$\lim_{n\rightarrow\infty} x=x_0$$ 
means there exists for all $\delta>0$ a $N$ such that for $n> N$
$$|x_n-x_0|<\delta,$$ 
and
$$\lim_{n\rightarrow \infty}f(x_n)=l$$ 
means that there exists for all $\epsilon>0$ a $N_2$ such that for $n>N_2$  
$$|f(x_n)-l|<\epsilon$$.
Why must these $N$ and $N_2$ exist? This is because of the definition of the limit of a sequence. Since $$\lim_{n\Rightarrow\infty} x=x_0 \Rightarrow \lim_{n\rightarrow \infty}f(x_n)=l, $$ we must have that $$|x_n-x_0|<\delta\Rightarrow |f(x_n)-l|<\epsilon.$$ There is nothing special with $x_n$. For all $x$ such that $|x-x_0|<\delta$ the above implication holds.  
