I have not seen this "style" of proof before of AoC/Zorn's lemma by thinking of partial functions $(A \rightarrow B)$ as monotone functions on $(A \cup \bot \rightarrow B)$.

§ Zorn's Lemma implies Axiom of Choice

If we are given Zorn's lemma and the set $A_i$, to build a choice function, we consider the collection of functions $(f: \prod_i A_i \rightarrow \rightarrow A_i \cup \bot)$ such that either $f(A_i) = \bot$ or $f(A_i) \in A_i$. This can be endowed with a partial order / join semilattice structure using the "flat" lattice, where $\bot < x$ for all $x$, and $\bot \sqcup x = x$.

For every chain of functions, we have a least upper bound, since a chain of functions is basically a collection of functions $f_i$ where each function $f_{i+1}$ is "more defined" than $f_i$.

Hence we can always get a maximal element $F$, which has a value defined at each $F(A_i)$. Otherwise, if we have $F(A_i) = \bot$, the element is not maximal, since it is dominated by a larger function which is defined at $A_i$.

Hence, we've constructed a choice function by applying Zorn's Lemma. Thus, Zorn's Lemma implies Axiom of Choice.