Birkhoff-Grothendieck: vector bundles on the projective line split

Base case. If $r=1$ then $E$ is invertible, so by [F2] there is a unique integer $a_1$ with $E\cong {\mathcal{O}}_X(a_1)$; this is a direct sum of one line bundle, and the multiset $\{a_1\}$ is determined by $E$.

The maximal line subbundle. Let $r\ge 2$ and assume the theorem known for all finite locally free modules of rank $r-1$. By [F4], applied to the nonzero module $E$, there is an integer $b$ with $H^0(X,E(-b))\mathrm{\ne }0$ and $H^0(X,E(-b-1))=0$, no line subbundle of $E$ has degree greater than $b$, and $E$ contains a line subbundle of degree $b$.

The normalized extension. Put $M:=E(-b)$, so that $H^0(X,M)\mathrm{\ne }0$ and $H^0(X,M(-1))=0$ by [F8] and step 1.2. Choose a nonzero global section $s$ of $M$; by [F6] the corresponding morphism $s^{\mathrm{♯}}:{\mathcal{O}}_X\to M$ is injective, and by [F5] (with $b=0$, its maximality hypothesis being exactly $H^0(X,M(-1))=0$) its cokernel $W:=M\mathrm{/}{\mathcal{O}}_X$ is a finite locally free ${\mathcal{O}}_X$-module of rank $r-1$. Thus $0\to {\mathcal{O}}_X\to M\to W\to 0$ is a short exact sequence.

The vanishing on the quotient. Twist the sequence of step 2.1 by ${\mathcal{O}}_X(-1)$: by [F8] this gives the short exact sequence $0\to {\mathcal{O}}_X(-1)\to M(-1)\to W(-1)\to 0$, whose long exact cohomology sequence by [F9] begins $0\to H^0({\mathcal{O}}_X(-1))\to H^0(M(-1))\to H^0(W(-1))\to H^1({\mathcal{O}}_X(-1))$. The two outer terms vanish by [F3] and the middle term vanishes by [F8] and step 1.2; exactness therefore forces $H^0(X,W(-1))=0$.

The quotient splits into twists of nonpositive degree. The module $W$ is finite locally free of rank $r-1$ by step 2.1, so the induction hypothesis of step 1.2 applied to $W$ gives $W\cong {⨁}_{i=1}^{r-1}{\mathcal{O}}_X(n_i)$ for integers $n_i$. By [F10] and [F3], $h^0(X,W(-1))={\sum }_{i=1}^{r-1}{h}^0(X,{\mathcal{O}}_X(n_i-1))$, and each summand equals $n_i$ when $n_i\ge 1$ and $0$ when $n_i\le 0$. Since $h^0(X,W(-1))=0$ by step 3.1 and all summands are nonnegative, every summand vanishes, so $n_i\le 0$ for every $i$.

Splitting off a line subbundle. The extension $0\to {\mathcal{O}}_X\to M\to W\to 0$ of step 2.1 has $W\cong {⨁}_i{\mathcal{O}}_X(n_i)$ with $n_i\le 0$ by step 4.1, so [F7] gives $M\cong {\mathcal{O}}_X\oplus W$. Twisting by ${\mathcal{O}}_X(b)$, which commutes with finite direct sums and satisfies ${\mathcal{O}}_X(b)\otimes {\mathcal{O}}_X(n)\cong {\mathcal{O}}_X(n+b)$ by [F8], yields $E\cong M(b)\cong {\mathcal{O}}_X(b)\oplus {⨁}_{i=1}^{r-1}{\mathcal{O}}_X(n_i+b)$, a direct sum of $r$ line bundles; this is the induction step, and with the base case of step 1.1 it proves that every finite locally free ${\mathcal{O}}_X$-module of rank $r\ge 1$ is a direct sum of line bundles.

Uniqueness of the multiset. Suppose $E\cong {⨁}_{i=1}^r{\mathcal{O}}_X(a_i)$. Twisting by ${\mathcal{O}}_X(m)$ and using [F8], [F10] and [F3] gives $h^0(X,E(m))={\sum }_{i=1}^r{h}^0(X,{\mathcal{O}}_X(a_i+m))={\sum }_{i=1}^r\max (a_i+m+1,0)$. Consequently the difference of consecutive values is $h^0(X,E(m))-h^0(X,E(m-1))=\mathrm{\#}\{i:a_i+m+1>0\}=\mathrm{\#}\{i:a_i\ge -m\}$, so for every integer $t$ the function determines the counting number $\mathrm{\#}\{i:a_i\ge t\}$ by evaluation at $m=-t$. The finitely many counting numbers $\mathrm{\#}\{i:a_i\ge t\}$ determine the multiset $\{a_i\}$, so the multiset is determined by $E$, equivalently by the function $m\mapsto h^0(X,E(m))$; in particular the decomposition is unique up to permutation of the summands.

Conclusion and choice accounting. Steps 1.1 and 5.1 prove the existence of the direct-sum decomposition for every rank $r\ge 1$, and step 6.1 proves that the multiset of degrees is determined by $E$, hence unique up to permutation; the translation to geometric vector bundles is [F1]. The Axiom of Choice is inherited only through the suppliers of the cited facts, as recorded in [F11]; the proof selects a section of a nonzero finite-dimensional space and a finite tuple of integers, and repeatedly reduces the rank by one, so no further infinite selection occurs.