A vector bundle on the projective line has a line subbundle of maximal degree

Nonemptiness of the section degrees. By [F4] the module $E$ is coherent, so [F3] applies with the ample invertible sheaf ${\mathcal{O}}_X(1)$ of [F2] and provides $m_0$ with $E(m)$ globally generated for all $m\ge m_0$. Since $E\mathrm{\ne }0$ and $X$ is nonempty, some stalk of $E(m)$ is nonzero, and global generation exhibits a global section with nonzero germ; hence $H^0(X,E(m))\mathrm{\ne }0$ for every $m\ge m_0$.

Boundedness below. Suppose $H^0(X,E(n))\mathrm{\ne }0$ and let $s\mathrm{\ne }0$ be a global section. By [F5] the section $s$ is a nonzero morphism $s^{\mathrm{♯}}:{\mathcal{O}}_X\to E(n)$; twisting by ${\mathcal{O}}_X(-n)$ yields a nonzero morphism ${\mathcal{O}}_X(-n)\to E$ by [F8], which is injective by [F7]. The left exact functor $H^0$ of [F5] therefore gives an injection $H^0(X,{\mathcal{O}}_X(-n))\hookrightarrow H^0(X,E)$, so ${\dim }_k{H}^0(X,{\mathcal{O}}_X(-n))\le h^0(E)$ with $h^0(E):={\dim }_k{H}^0(X,E)<\mathrm{\infty }$ by [F4]. If $n\le 0$, then by [F6] the left side is $-n+1$, so $-n+1\le h^0(E)$, that is $n\ge 1-h^0(E)$. If $n\ge 1$, then $n\ge 1$; and since $h^0(E)\ge 0$ we get $n\ge 1-h^0(E)$ in this case too. Hence every $n$ with $H^0(X,E(n))\mathrm{\ne }0$ satisfies $n\ge B$ for the integer $B:=1-h^0(E)$, and the set of such $n$ is nonempty by step 1.1 and bounded below.

The extremal degree. The set $S=\{n\in \mathbb{Z}:H^0(X,E(n))\mathrm{\ne }0\}$ is a nonempty subset of $\mathbb{Z}$ bounded below, so it has a minimum $a$. Put $b:=-a$. Then $H^0(X,E(-b))=H^0(X,E(a))\mathrm{\ne }0$, and $H^0(X,E(-b-1))=H^0(X,E(a-1))=0$, since $a-1\mathrm{\notin }S$ by minimality.

The maximal map is a subbundle. Fix any nonzero morphism $\phi :{\mathcal{O}}_X(b)\to E$. It is injective by [F7]. Let $p$ be a closed point and choose local frames for ${\mathcal{O}}_X(b)$ and $E$ near $p$; write the coefficient vector of $\phi$ in these frames as $(q_1,\dots ,q_r)$. Suppose every $q_i$ lies in the maximal ideal of ${\mathcal{O}}_{X,p}$. By [F10], this local ring is a DVR with uniformizer $\pi$, so every $q_i\mathrm{/}\pi$ is regular at $p$. After shrinking a neighborhood $U$ of $p$, these quotients are regular sections and ${\mathcal{O}}_X(p){\mathrm{\mid }}_U={\pi }^{-1}{\mathcal{O}}_U$. Define a morphism ${\mathcal{O}}_X(b)\otimes {\mathcal{O}}_X(p){\mathrm{\mid }}_U\to E{\mathrm{\mid }}_U$ by sending the frame $e\otimes {\pi }^{-1}$ to $\phi (e)\mathrm{/}\pi$. On $X\setminus \{p\}$ use the identification ${\mathcal{O}}_X(p)={\mathcal{O}}_X$ and the original $\phi$. On the overlap $U\setminus \{p\}$, $\pi$ is a unit and the maps agree, so they glue to a global morphism ${\mathcal{O}}_X(b)\otimes {\mathcal{O}}_X(p)\to E$. It is nonzero because its restriction at the generic point agrees with $\phi$. By [F10] its source is isomorphic to ${\mathcal{O}}_X(b+d)$ for $d=[\kappa (p):k]>0$. Thus $H^0(X,E(-b-d))\mathrm{\ne }0$, contradicting minimality of $a=-b$. Therefore at least one $q_i$ is a unit at every closed point $p$. On a neighborhood where that coefficient remains a unit, elementary row operations make the image a direct summand of $E$, so the quotient is locally free there. At the generic point the nonzero map is an inclusion of a one-dimensional subspace into a vector space and is likewise a direct summand after restricting to a neighborhood. Hence $\phi$ has locally free quotient and its image is a line subbundle of degree $b$. Since $\phi$ was arbitrary, every nonzero map ${\mathcal{O}}_X(b)\to E$ has this property.

Maximality. Let $L\subseteq E$ be any line subbundle of degree $d$. By the Picard classification in [F10], $L\cong {\mathcal{O}}_X(d)$. Its inclusion is nonzero, so after twisting by ${\mathcal{O}}_X(-d)$ it gives a nonzero morphism ${\mathcal{O}}_X\to E(-d)$ by [F8], hence a nonzero global section of $E(-d)$ by [F5]. Thus $-d\in S$. By step 3.1, $-d\ge a=-b$, so $d\le b$: no line subbundle has degree greater than $b$.

Conclusion. Steps 1.1 and 2.1 show that $S$ is nonempty and bounded below, step 3.1 produces its minimum $a$ with $b=-a$ and the two vanishing statements, step 4.1 proves that every nonzero maximal-degree map has locally free quotient, and step 4.2 proves maximality among line subbundles. Choice is inherited only from the suppliers recorded in [F9].