A submodule of an arbitrary-rank free module over a PID is free

Use [L4] to well-order $W$. For $a\in W$ let $F_{\le a}$ and $F_{<a}$ be the spans of the corresponding basis initial segments. Let $I_a$ be the image of $N\cap F_{\le a}$ under the $a$-coordinate map. This image is an ideal because the coordinate map is $R$-linear.

If $I_a\mathrm{\ne }0$, [L1] supplies a nonzero generator $r_a$ and the definition of the image supplies $x_a\in N\cap F_{\le a}$ with $a$-coordinate $r_a$. The sets of such pairs $(r_a,x_a)$ are nonempty and indexed by a subset of $W$; use [L3] to choose them simultaneously. This is the second use of AC, after well-ordering the basis.

If $y\in N\cap F_{\le a}$ and $I_a=0$, then $y\in F_{<a}$. If $I_a\mathrm{\ne }0$, write its $a$-coordinate as $c{r}_a$; then $y-c{x}_a\in N\cap F_{<a}$. In either case the remainder has finite support below $a$.

Induct on $a$ using [L5] to show that $N\cap F_{\le a}$ is spanned by the chosen $x_b$ with $b\le a$. By step 3.1 it suffices to handle a finite-support remainder in $F_{<a}$. A zero remainder needs no generators; otherwise its support has a greatest element $b<a$, so the induction hypothesis at $b$ applies. This includes least and limit positions without selecting a cofinal sequence. Every nonzero element of $N$ has a greatest support element, so the chosen family spans $N$.

In a nonzero finite relation among the chosen $x_a$, take the greatest index $a$ with nonzero coefficient $c_a$. Its $a$-coordinate is $c_a{r}_a$: all smaller-index vectors have zero coordinate there. Since $R$ is a domain and $r_a\mathrm{\ne }0$, this coordinate is nonzero, a contradiction. Thus the family is independent and is a basis by step 4.1. If $W$ or $N$ is empty or zero as applicable, the same argument gives the empty basis.