Finite-dimensional subspaces admit projections without Choice

Apply F1 to the empty independent subset of $U$ to obtain a finite basis $u_1,\dots ,u_r$. This is independent in $V$, so apply F1 with subspace $V$ to extend it to $u_1,\dots ,u_r,w_1,\dots ,w_s$. Every vector has an expansion in this basis; two expansions agree coefficientwise because their difference is a zero linear combination of an independent family.

Define $P({\sum }_{j=1}^r{a}_j{u}_j+{\sum }_{\mathrm{\ell }=1}^s{b}_{\mathrm{\ell }}{w}_{\mathrm{\ell }})={\sum }_{j=1}^r{a}_j{u}_j$. The uniqueness just proved makes $P$ a well-defined function $V\to V$. If $v,v^{\mathrm{\prime }}$ have $u$-coordinates $a_j,a_j^{\mathrm{\prime }}$, then $cv+d{v}^{\mathrm{\prime }}$ has $u$-coordinates $c{a}_j+d{a}_j^{\mathrm{\prime }}$. Consequently $P(cv+d{v}^{\mathrm{\prime }})={\sum }_j(c{a}_j+d{a}_j^{\mathrm{\prime }})u_j=cP(v)+dP(v^{\mathrm{\prime }})$, so $P$ is linear.

Each $P(v)$ belongs to $U$. For $u\in U$, its basis expression uses only the $u_j$, so $P(u)=u$. Thus every $u\in U$ is in the image, and $\mathrm{im}P=U$. Since $P(v)\in U$, also $P(P(v))=P(v)$.

If $U=0$, then $r=0$ and the formula gives $P=0$. If $U=V$, no added vectors are needed and $P={\mathrm{id}}_V$. If $V=0$, both lists are empty and these formulas coincide. Only two applications of the choice-free finite extension result and finite enumerations were used; no simultaneous choice over an infinite family occurs.