Sequential criterion of the limit of a function, extended to include infinity Is the following theorem correct? It is an extended version of Theorem 4.1.1 of Strichartz's the Way of Analysis, or this theorem from mathonline. The difference is that I have tried to include the case $y= \pm \infty$, as well as the possibility that the limit itself is $\pm \infty$.
When we consider a limit point in $\bar{\mathbb{R}} = \mathbb{R} \cup \lbrace -\infty, \infty \rbrace$, we consider the topology on $\bar{\mathbb{R}}$ that makes it homeomorphic to $[-1,1]$, so that e.g. $\infty$ is a limit point of $\mathbb{R}$. 
Theorem
Let $D\subseteq \mathbb{R}$, let $y \in \bar{\mathbb{R}}$ be a limit point of $D$ in $\bar{\mathbb{R}}$ and let $f: D \rightarrow \mathbb{R}$ be a function. $\lim_{x \rightarrow y} f(x)$ exists iff for every sequence $(x_i)_{i=1}^\infty \subseteq D \setminus \lbrace y \rbrace$ with $\lim_{i \rightarrow \infty} x_i = y$, $\lim_{i \rightarrow \infty}f(x_i)$ exists. If either of the statements of this equivalence holds, then the limit $\lim_{x \rightarrow y} f(x)$ and the sequential limits $\lim_{i \rightarrow \infty} f(x_i)$ are all equal.
I have tried to prove the theorem using the substitution theorem (Theorem 4.1.4 in Mathematical Analysis by Canuto and Tabacco), properties of $f(x) = \vert \frac{1}{x} \vert$ and the original theorem that I am trying to extend. It was all a bit tedious and the proof became quite long. I could provide more details, but I hope I have shown enough effort to ask if the formulation of the theorem is correct. I want to be sure I did not make a mistake, like that the convergence of sequences is not enough and we need for example all nets have to converge.
 A: 
we consider the topology on $\bar{\mathbb{R}}$ that makes it homeomorphic to $[-1,1]$

So in fact you are dealing with $[-1,1]$, thus your claim should be true. Its topological nature its simple and it should follow from the following general 
Proposition. Let $X$ and $Y$ be topological spaces, the space $Y$ is Hausdorff, $D\subset X$, $y\in \overline{D}\setminus D$ and $f:D\to Y$ be a map. If there is a countable base at the point $y$ then $\lim_{x\to y} f(x)$ exists iff for every sequence $(x_i)_{i=1}^\infty \subseteq D \setminus \lbrace y \rbrace$ with $\lim_{i \rightarrow \infty} x_i = y$, $\lim_{i \rightarrow \infty}f(x_i)$ exists. Moreover, if either of the statements of this equivalence holds then the limit $\lim_{x \rightarrow y} f(x)$ and the sequential limits $\lim_{i \rightarrow \infty} f(x_i)$ are all equal.
Proof. Since necessity of the equivalence is evident, it remains to prove that if all sequential limits $\lim_{i \rightarrow \infty} f(x_i)$ exist then the limit $\lim_{x \rightarrow y} f(x)$ exists and the sequential limits $\lim_{i \rightarrow \infty} f(x_i)$ are all equal to it. Indeed, let $\{U_i\}$ be a countable base at the point $y$ such that $U_i\supset U_{i+1}$ for each $i$. For each $i$ pick a point $x_i\in U_i\cap D$. Then $\lim_{i \rightarrow \infty} x_i=y$, so there exists a limit $\lim_{i \rightarrow \infty}f(x_i)=z$. 
Let $(y_i)_{i=1}^\infty$ be any sequence of points of $D$ converging to $y$. Consider a sequence $(z_i)_{i=1}^\infty=(x_1,y_1,x_2, y_2,\dots)$. There exists a limit $\lim_{i \rightarrow \infty}f(z_i)=z’$. Since $z’$ is also a limit of the sequence $(f(x_i))_{i=1}^\infty$, and the space $Y$ is Hausdorff, $z’=z$. Thus $z$ is also a limit of the sequence $(f(y_i))_{i=1}^\infty$. 
Now assume that $\lim_{x\to y} f(x)$ does not equal to $z$. Then there exists a neigborhood $O_z$ of the point $z$ such that for each $i$ there exists a point $y_i\in U_i\cap D$ with $f(y_i)\not\in O_z$. Then $z$ is not a limit of the sequence $(f(y_i))_{i=1}^\infty$, a contradiction. $\square$ 
Update. Countable base at a point $y$ is a countable family $(U_i)$ of its neighborhoods such that for any neighborhood $U$ of the point $y$ there exists $U_i\subset U$. The condition “there exists a (countable) sequence $(U_i)$ of open sets of $X$ so that $\bigcap_{i=1}^\infty U_i=\{y\}$ corresponds to so-called countable pseudocharacter $\psi(y,X)$ of the point $y$ in the space $X$, which is weaker than the existence of a countable base at $y$ (which corresponds to countable character $\chi(y,X)$ of $y$). 
In the proposition, in general, we cannot replace countability of $\chi(y)$ by countability of $\psi(y)$. Indeed, define a topology $\tau$ on the set $\Bbb R$ by putting a set $U\in\tau$ iff $U=V\setminus C$  for some set $V$ open in the standard topology of $\Bbb R$ and (at most) countable set $C$. Let $Y=\{0,1\}$ endowed with the discrete topology. For each natural $n$ put $D_n=[2^{-n},2^{-n}+2^{-n-1}]$ and $D=\bigcup D_n$. Define a function $f:D\to Y$ by putting $f|D_n=0$, if $n$ is even and $f|D_n=1$, if $n$ is odd. Then $0\in\overline{D}$, $\psi(0,X)$ is countable, and the condition “for every sequence $(x_i)_{i=1}^\infty \subseteq D \setminus \lbrace y \rbrace$ with $\lim_{i \rightarrow \infty} x_i = y$, $\lim_{i \rightarrow \infty}f(x_i)$ exists” trivially holds because no sequence of points of $D$ converge to $x$. Nevertheless, $\lim_{x\to y} f(x)$ doesn’t exist.
