[proofplan]
We construct the map from the localization by evaluating fractions on the locus where $f$ is nonzero, and first check that localization equality gives the same function. For surjectivity, we represent a regular function locally by quotients, shrink to distinguished opens using [citetheorem:9424], and use the affine [closed set](/page/Closed%20Set) radical ideal correspondence [citetheorem:9414] to convert containments of zero sets into powers in ideals. A finite distinguished cover lets us clear denominators uniformly, produce compatible local numerators, and glue them into a single fraction with denominator a power of $f$; the overlap compatibility uses the fact that coordinate rings of affine varieties are reduced [citetheorem:9415]. Injectivity follows by showing that a numerator vanishing on all of $D(f)$ becomes killed by a power of $f$.
[/proofplan]
[step:Dispose of the empty distinguished open]
Let $A=k[X]$. If $f=0$ in $A$, then $D(f)=\varnothing$. Under the standard convention that the ring of regular functions on the empty [open set](/page/Open%20Set) is the zero ring, $\mathcal O_X(\varnothing)=0$. Also $A_f=A[1/f]$ is the zero ring, because the multiplicative set generated by $f$ contains $0$. Thus the asserted map is an isomorphism in this case.
For the rest of the proof, assume $f\ne 0$ in $A$.
[/step]
[step:Define the evaluation homomorphism from the localization]
For $a\in A$ and $m\in \mathbb N\cup\{0\}$, define
\begin{align*}
\Phi\left(\frac{a}{f^m}\right):D(f)&\longrightarrow k
\end{align*}
\begin{align*}
p&\longmapsto \frac{a(p)}{f(p)^m}.
\end{align*}
This is a regular function on $D(f)$ because every point of $D(f)$ has a neighbourhood on which the denominator $f^m$ is nonzero.
We check that $\Phi$ is well-defined. Suppose
\begin{align*}
\frac{a}{f^m}=\frac{a'}{f^{m'}}
\end{align*}
in $A_f$. By the definition of localization, there exists $q\in \mathbb N\cup\{0\}$ such that
\begin{align*}
f^q(f^{m'}a-f^m a')=0
\end{align*}
in $A$. Evaluating at any $p\in D(f)$ gives
\begin{align*}
f(p)^q(f(p)^{m'}a(p)-f(p)^m a'(p))=0.
\end{align*}
Since $f(p)\ne 0$, division by $f(p)^{q+m+m'}$ gives
\begin{align*}
\frac{a(p)}{f(p)^m}=\frac{a'(p)}{f(p)^{m'}}.
\end{align*}
Hence $\Phi$ is well-defined. The formulas for addition, multiplication, and scalar multiplication of fractions show directly that $\Phi$ is a $k$-algebra homomorphism.
[guided]
We want a map from the localized ring $A_f$ to functions on the open set where $f$ does not vanish. The only possible definition is to evaluate a fraction pointwise. For $a\in A$ and $m\in \mathbb N\cup\{0\}$, set
\begin{align*}
\Phi\left(\frac{a}{f^m}\right):D(f)&\longrightarrow k
\end{align*}
\begin{align*}
p&\longmapsto \frac{a(p)}{f(p)^m}.
\end{align*}
This expression is defined for every $p\in D(f)$ because the definition of $D(f)$ says precisely that $f(p)\ne 0$. It is also regular on $D(f)$, since it is locally a quotient of coordinate functions with denominator nonzero.
The point requiring verification is well-definedness: the same element of $A_f$ can have many fraction representatives. Suppose
\begin{align*}
\frac{a}{f^m}=\frac{a'}{f^{m'}}
\end{align*}
in $A_f$. By the [equivalence relation](/page/Equivalence%20Relation) defining localization, there is an integer $q\ge 0$ such that
\begin{align*}
f^q(f^{m'}a-f^m a')=0
\end{align*}
in $A$. Since elements of $A=k[X]$ are regular functions on $X$, evaluating this equality at a point $p\in D(f)$ gives
\begin{align*}
f(p)^q(f(p)^{m'}a(p)-f(p)^m a'(p))=0.
\end{align*}
Now $f(p)\ne 0$, so the scalar $f(p)^{q+m+m'}$ is nonzero in the field $k$. Dividing gives
\begin{align*}
\frac{a(p)}{f(p)^m}=\frac{a'(p)}{f(p)^{m'}}.
\end{align*}
Thus equivalent fractions define the same function. Finally, addition and multiplication of fractions in $A_f$ are sent to pointwise addition and multiplication of the corresponding functions, so $\Phi$ is a $k$-algebra homomorphism.
[/guided]
[/step]
[step:Represent a regular function on a finite distinguished cover]
Let
\begin{align*}
\varphi:D(f)\longrightarrow k
\end{align*}
be a regular function. For each $p\in D(f)$, regularity gives an open neighbourhood $U_p\subset D(f)$, elements $\alpha_p,\beta_p\in A$, and the condition $\beta_p(q)\ne 0$ for all $q\in U_p$, such that
\begin{align*}
\varphi(q)=\frac{\alpha_p(q)}{\beta_p(q)}
\end{align*}
for all $q\in U_p$.
By [citetheorem:9424], [distinguished opens form a basis](/theorems/9424) for the Zariski topology on $X$. Hence, for each $p\in D(f)$, choose $g_p\in A$ such that
\begin{align*}
p\in D(g_p)\subset U_p\cap D(\beta_p)\cap D(f).
\end{align*}
The inclusion $D(g_p)\subset D(\beta_p)$ is equivalent to
\begin{align*}
V_X(\beta_p)\subset V_X(g_p).
\end{align*}
By the affine closed set radical ideal correspondence [citetheorem:9414], there exist $s_p\in \mathbb N$ and $c_p\in A$ such that
\begin{align*}
g_p^{s_p}=c_p\beta_p.
\end{align*}
Therefore on $D(g_p)$,
\begin{align*}
\varphi=\frac{\alpha_p c_p}{g_p^{s_p}}.
\end{align*}
The space $X$ is Noetherian by [citetheorem:9411], and every subspace of a Noetherian [topological space](/page/Topological%20Space) is quasi-compact. Hence $D(f)$ is quasi-compact, so finitely many of these opens cover it. Write them as
\begin{align*}
D(g_1),\dots,D(g_r).
\end{align*}
For each $i\in\{1,\dots,r\}$, choose $a_i\in A$ and $e_i\in\mathbb N$ such that
\begin{align*}
\varphi=\frac{a_i}{g_i^{e_i}}
\end{align*}
on $D(g_i)$. Let $E=\max\{e_1,\dots,e_r\}$. Replacing $a_i$ by $a_i g_i^{E-e_i}$ gives
\begin{align*}
\varphi=\frac{a_i}{g_i^E}
\end{align*}
on $D(g_i)$ for every $i$.
[/step]
[step:Clear the overlap errors to obtain exact compatibility]
For $i,j\in\{1,\dots,r\}$, the two formulas agree as functions on
\begin{align*}
D(g_i)\cap D(g_j)=D(g_i g_j).
\end{align*}
Define $h_{ij}\in A$ and $s_{ij}\in A$ by
\begin{align*}
h_{ij}=a_i g_j^E-a_j g_i^E
\end{align*}
and
\begin{align*}
s_{ij}=g_i g_j.
\end{align*}
The equality of the two local formulas says that $h_{ij}$ vanishes at every point of $D(s_{ij})$. If $p\in X\setminus D(s_{ij})$, then $s_{ij}(p)=0$, while if $p\in D(s_{ij})$, then $h_{ij}(p)=0$. Hence the product $s_{ij}h_{ij}$ vanishes at every point of $X$. Since $A=k[X]$ is reduced by [citetheorem:9415], the coordinate-ring element represented by a function vanishing on all of $X$ is zero. Therefore
\begin{align*}
(g_i g_j)(a_i g_j^E-a_j g_i^E)=0
\end{align*}
in $A$ for every pair $(i,j)$.
Choose $M=1$. Replace $a_i$ by $a_i g_i^M$ and replace $E$ by
\begin{align*}
R=E+M.
\end{align*}
The local expression represented by numerator $a_i$ and denominator $g_i^E$ is unchanged on $D(g_i)$. Indeed, after the replacement the corresponding functions agree because $g_i$ is nowhere zero on $D(g_i)$.
After this replacement, the compatibility difference is
\begin{align*}
a_i g_i^M g_j^{E+M}-a_j g_j^M g_i^{E+M}
=(g_i g_j)^M(a_i g_j^E-a_j g_i^E).
\end{align*}
Since $M=1$, this is zero by the already proved identity
\begin{align*}
(g_i g_j)(a_i g_j^E-a_j g_i^E)=0.
\end{align*}
Thus
\begin{align*}
a_i g_j^R=a_j g_i^R
\end{align*}
in $A$ for all $i,j$.
[/step]
[step:Use the cover to express a power of $f$ in the generated ideal]
Because the opens $D(g_1),\dots,D(g_r)$ cover $D(f)$, a point of $X$ at which every $g_i$ vanishes cannot lie in $D(f)$. Therefore
\begin{align*}
V_X(g_1,\dots,g_r)\subset V_X(f).
\end{align*}
Replacing the generators by their $R$-th powers does not change the common zero set:
\begin{align*}
V_X(g_1^R,\dots,g_r^R)=V_X(g_1,\dots,g_r).
\end{align*}
By [citetheorem:9414], there exist $N\in\mathbb N$ and $b_1,\dots,b_r\in A$ such that
\begin{align*}
f^N=\sum_{i=1}^r b_i g_i^R.
\end{align*}
[/step]
[step:Glue the local fractions into one global fraction]
Define $a\in A$ by
\begin{align*}
a=\sum_{i=1}^r b_i a_i.
\end{align*}
Fix $j\in\{1,\dots,r\}$. Using the compatibility relations from the preceding step,
\begin{align*}
g_j^R a=\sum_{i=1}^r b_i a_i g_j^R.
\end{align*}
Since $a_i g_j^R=a_j g_i^R$ for every $i$, this becomes
\begin{align*}
g_j^R a=\sum_{i=1}^r b_i a_j g_i^R.
\end{align*}
Factoring out $a_j$ and using the expression for $f^N$, we get
\begin{align*}
g_j^R a=a_j f^N.
\end{align*}
On $D(g_j)$, the element $g_j$ is nowhere zero, so this identity gives
\begin{align*}
\frac{a}{f^N}=\frac{a_j}{g_j^R}
\end{align*}
as regular functions on $D(g_j)$. Since the opens $D(g_j)$ cover $D(f)$, the fraction $a/f^N\in A_f$ maps to $\varphi$ on all of $D(f)$. Thus $\Phi$ is surjective.
[guided]
The finite cover has reduced the problem to a gluing problem. We have local formulas
\begin{align*}
\varphi=\frac{a_i}{g_i^R}
\end{align*}
on $D(g_i)$, and the previous step arranged the exact algebraic compatibility
\begin{align*}
a_i g_j^R=a_j g_i^R
\end{align*}
in $A$ for all $i,j$. We also know, from the fact that the $D(g_i)$ cover $D(f)$ and from [citetheorem:9414], that some power of $f$ lies in the ideal generated by the $g_i^R$:
\begin{align*}
f^N=\sum_{i=1}^r b_i g_i^R.
\end{align*}
This identity is the algebraic substitute for a [partition of unity](/page/Partition%20of%20Unity). It lets us combine the local numerators $a_i$ into one global numerator.
Define $a\in A$ by
\begin{align*}
a=\sum_{i=1}^r b_i a_i.
\end{align*}
We now check that the single fraction $a/f^N$ restricts to the known local fraction on every member of the cover. Fix $j\in\{1,\dots,r\}$. Multiplying by $g_j^R$ gives
\begin{align*}
g_j^R a=\sum_{i=1}^r b_i a_i g_j^R.
\end{align*}
The compatibility relation allows us to replace $a_i g_j^R$ by $a_j g_i^R$ in each summand:
\begin{align*}
g_j^R a=\sum_{i=1}^r b_i a_j g_i^R.
\end{align*}
Now factor out $a_j$:
\begin{align*}
g_j^R a=a_j\sum_{i=1}^r b_i g_i^R.
\end{align*}
Using the identity for $f^N$, this becomes
\begin{align*}
g_j^R a=a_j f^N.
\end{align*}
On $D(g_j)$, the function $g_j$ is nowhere zero, so division by $g_j^R f^N$ is legitimate pointwise on $D(g_j)$. Hence
\begin{align*}
\frac{a}{f^N}=\frac{a_j}{g_j^R}
\end{align*}
as regular functions on $D(g_j)$. Since the sets $D(g_j)$ cover $D(f)$, the fraction $a/f^N$ represents $\varphi$ everywhere on $D(f)$. This proves surjectivity of $\Phi$.
[/guided]
[/step]
[step:Show that a fraction mapping to zero is zero in the localization]
Suppose
\begin{align*}
\Phi\left(\frac{a}{f^m}\right)=0
\end{align*}
for some $a\in A$ and $m\in\mathbb N\cup\{0\}$. Then $a(p)=0$ for every $p\in D(f)$, because $f(p)^m\ne 0$ on $D(f)$. We claim that $fa$ vanishes at every point of $X$. If $p\in D(f)$, then $a(p)=0$, so $(fa)(p)=0$. If $p\in X\setminus D(f)$, then $f(p)=0$, so again $(fa)(p)=0$. Since $A=k[X]$ is reduced by [citetheorem:9415], this pointwise-zero regular function is the zero element of $A$, so
\begin{align*}
fa=0
\end{align*}
in $A$. By the defining equivalence relation in the localization $A_f$, this means
\begin{align*}
\frac{a}{f^m}=0
\end{align*}
in $A_f$. Therefore $\Phi$ is injective.
[guided]
We must prove that a fraction whose associated function is zero on $D(f)$ is already zero in the localization. Assume
\begin{align*}
\Phi\left(\frac{a}{f^m}\right)=0
\end{align*}
for some $a\in A$ and $m\in\mathbb N\cup\{0\}$. This means that for every $p\in D(f)$,
\begin{align*}
\frac{a(p)}{f(p)^m}=0.
\end{align*}
Because $f(p)\ne 0$ on $D(f)$, the scalar $f(p)^m$ is nonzero in $k$, and therefore $a(p)=0$ for every $p\in D(f)$.
The useful global consequence is not a containment involving $V_X(f)$. Instead, the product $fa$ vanishes everywhere on $X$. If $p\in D(f)$, then $a(p)=0$, so $(fa)(p)=0$. If $p\in X\setminus D(f)$, then by definition of $D(f)$ we have $f(p)=0$, so $(fa)(p)=0$ again. Thus $fa$ is the zero function on all of $X$.
By [citetheorem:9415], the coordinate ring $A=k[X]$ is reduced, so a coordinate-ring element represented by a regular function vanishing at every point of $X$ is zero in $A$. Hence
\begin{align*}
fa=0
\end{align*}
in $A$. In the localization $A_f$, this is exactly the condition that the fraction is zero: the defining equivalence relation gives
\begin{align*}
\frac{a}{f^m}=0
\end{align*}
because a power of $f$, namely $f^1$, kills the numerator $a$. Therefore $\Phi$ is injective.
[/guided]
Since $\Phi$ is a well-defined $k$-algebra homomorphism that is both surjective and injective, it is an isomorphism. This proves the theorem.
[/step]