I'm trying to prove a theorem from Olver's Applications of Lie Groups to Differential Equations.
It's supposed to be an "easy" consequence of the Implicit Function Theorem but I honestly can't see how to prove it from that.
Let $M$ and $N$ smooth manifolds of dimension $m$ and $n$ respectively. Let $F: M \rightarrow N$ be of maximal rank at $x_0 \in M$. Then there are local coordinates $x = (x^1, ... , x^m)$ near $x_0$, and $y = (y^1,...,y^n)$ near $y_0 = F(x_0)$ such that in these coordinates F has the simple form:
$y = (x^1, .. ,x^m,0,...,0)$, if n > m
or
$y = (x^1,...,x^n)$, if n $\leqslant$ m
Now to apply the Implicit Function Theorem we need an $f: \mathbb{R}^{m+n} \rightarrow \mathbb{R}^n$ but I am not exactly sure how to construct this.
I am not sure if this helps, but since $F$ has maximal rank at $x_0\in M$ either $m<n$ in which case $F$ is an immersion, $m>n$ in which case $F$ is a submersion or $m=n$ in which case $F$ is a diffeomorphism. Any immersion or submersion is locally of the form, respectively, what you gave above. This is called the immersion (or submersion) theorem. If $m=n$ then you can apply the inverse function theorem to get your above form.