Solution (source code)

= Solution

Let $r=\operatorname{rank}F$ and $s=\operatorname{rank}E$. Around any $p$, choose a <local frame> $f_1,\ldots,f_r$ of the <vector subbundle> $F$. Choose additional smooth sections $e_{r+1},\ldots,e_s$ of $E$ which complement these vectors at $p$. They can be obtained by constant-coordinate sections in a <vector bundle trivialization>. The <determinant> of the resulting frame is nonzero at $p$, hence on a sufficiently small neighborhood. Thus
$$
f_1,\ldots,f_r,e_{r+1},\ldots,e_s
$$
is an adapted <local frame> of $E$ near $p$.

On the fiberwise quotient, the classes $[e_{r+1}],\ldots,[e_s]$ form a <basis>. Give the <quotient vector bundle> its local coordinates by
$$
\sum_{j=r+1}^s a_j[e_j(p)]\longleftrightarrow(p,a_{r+1},\ldots,a_s).
$$
An overlap between adapted frames has a smooth <transition function of a vector bundle> represented by an invertible block upper triangular <matrix>,
$$
\begin{pmatrix}A&B\\0&D\end{pmatrix}.
$$
The zero lower-left block expresses that both sets of first $r$ frame vectors span $F$. Its lower-right block $D$ is smooth and invertible. Passing to quotient coordinates removes the upper block, leaving precisely the transition $D$. These lower-right blocks satisfy the cocycle identity because the original transition matrices do. Consequently they define a compatible smooth bundle atlas of rank $s-r$. This proves \b[$E/F$ is a smooth <vector bundle>], and its fiberwise quotient map $q:E\to E/F$ is a smooth <vector bundle morphism>. The construction is independent of the adapted frames: any two choices have the same type of compatible transition. The usual quotient topology agrees with this atlas, since in adapted coordinates $q$ is an open linear projection on each <fiber>.