Corollary

— Let $f_i(Y_1, Y_2, \ldots, Y_q, X_1, X_2, \ldots, X_p)$ ($1 \leq i \leq q$) be $q$ formal power series without constant term in $A[[Y_1, \ldots, Y_q, X_1, \ldots, X_p]]$. If the constant term of the formal power series $D = \det \left( \frac{\partial f_i}{\partial Y_j} \right)$ is invertible in $A$, then there exists precisely one system of $q$ formal power series $u_1(X_1, \ldots, X_p), \ldots, u_q(X_1, \ldots, X_p)$ such that

Put $f_{q+1} = X_1, \ldots, f_{q+p} = X_p$, $f = (f_1, \ldots, f_{p+q})$, then $\det T_f$ is equal to the constant term of $D$, hence invertible in $A$; therefore $T_f$ is invertible. By Prop. 10 there exist formal power series without constant term such that on writing we have $f \circ g = g \circ f = 1_{p+q}$. The relation $f \circ g = 1_{p+q}$, in particular gives Hence Now put substituting 0 for each $Y_i$ in (30) we obtain the desired relation (29).

Conversely, suppose that the formal power series $u_1, \ldots, u_q$ in the ring $A[[X_1, \ldots, X_p]]$ satisfy the relation (29). The relation $g \circ f = 1_{p+q}$ implies

and substituting $u_i$ for $Y_i$ for $1 \leq i \leq q$ in (32), we obtain (31), whence the uniqueness of the solution of the system (29).