I am working on Olver's book Applications of Lie Groups to Differential Equations and I have been trying to prove how a prolongation of a smooth action $(g,x,u) \mapsto g \cdot (x,u)= (\Xi_{g}(x,u),\Phi_{g}(x,u))=(\tilde{x},\tilde{u})$ on a manifold $M$ is again smooth. The prolongation of the group action on the jet-space $M^{n}$ is defined as $(g,(x,u^{(n)})) \mapsto pr^{(n)} g \cdot (x,u^{(n)})=pr^{(n)} (g \cdot f) (\tilde{x})$ where $f$ is a function whose derivatives are equal to the u-components of the point $(x,u^{(n)})$ and where $(g \cdot f)=[\Phi_{g} \circ (1 \times f)]\circ[\Xi_{g} \circ (1 \times f)]^{-1}(\tilde{x})$ supposes the inverse is well-defined (this is always possible in a neighborhood of the identity $e$).
I saw that Kunzinger in some notes he wrote on the subject says that prolongation of group actions are smooth in virtue of the implicit function theorem and the fact that they are defined in terms of prolongation of functions. Basically, his idea is the following, but I am not sure I understand it. Suppose $g$ is closed enough to the group identity so $[\Xi_{g} \circ (1 \times f)]^{-1}$ is well-defined around a point $(x,u^{(n)})$ where $f$ is the nth-order taylor polynomial whose coefficients are composed of the components $u_{J}^{\alpha}$ of the said point. Then we can consider that $f$ (and $[\Xi_{g} \circ (1 \times f)]$?) depend smoothly on $pq^{(n)}$ parameters $\alpha_{i}$ which take the $u_{J}^{\alpha}$ as values. In consequence, the inverse $[\Xi_{g} \circ (1 \times f)]^{-1}$ will also depend smoothly on the parameters $\alpha_{i}$.
I wonder if this supposes we are working on some space of functions. I am not sure I understand. Is it correct to say the following? Suppose the taylor polynomial corresponding to the point $(x,u^{(n)})$ is also considered as a function of the parameters $\alpha_{i}$ and so $f(x) \equiv f_{\alpha}(x)$ where alpha is the $pq^{n}$-tuple whose value are the $u_{J}^{\alpha}$. Then, we have the following equalities:
$pr^{(n)} g \cdot (x,u^{(n)})=pr^{(n)} (g \cdot f) (\tilde{x})=pr^{(n)} (g \cdot f) (\tilde{x})=[\Phi_{g} \circ (1 \times f_{\alpha})]\circ[\Xi_{g} \circ (1 \times f_{\alpha})]^{-1}(\tilde{x})=pr^{(n)} (g \cdot f) (\tilde{x})=pr^{(n)}([\Phi_{g} \circ (1 \times f_{\alpha})]\circ[\Xi_{g} \circ (1 \times f_{\alpha})]^{-1})([\Xi_{g} \circ (1 \times f_{\alpha})](x))$
where the last member depends smoothly on $x$ and the $u_{J}^{\alpha}$.