Solution (source code)

= Solution

At a point where $df$ is surjective, choose charts and reorder the domain coordinates so that an $\ell\times\ell$ minor of the derivative is invertible. The map $F=(f_1,\ldots,f_\ell,x_{\ell+1},\ldots,x_k)$ has invertible derivative. By the <inverse function theorem> it gives local coordinates, in which $f$ is the projection $(u_1,\ldots,u_k)\mapsto(u_1,\ldots,u_\ell)$. This is the <submersion theorem>.