形式群

$F(X,Y)=\sum_{i,j\geq0}a_{ij}X^iY^j$ と書く。$F(X,0)=X$ から
$$ a_{10}=1,\qquad a_{i0}=0\quad(i\neq1) $$
を得る。同様に $F(0,Y)=Y$ から
$$ a_{01}=1,\qquad a_{0j}=0\quad(j\neq1) $$
を得る。従って $X+Y$ 以外に残り得る単項式は $i,j\geq1$ のものだけである。

係数写像 $R\to S$ は多変数形式的冪級数環の写像
$$ R[\![X_1,\ldots,X_r]\!]\longrightarrow S[\![X_1,\ldots,X_r]\!] $$
を誘導し、和、積、および定数項が $0$ の冪級数の代入を保つ。従って $F(X,0)=X$、$F(0,Y)=Y$、結合律、可換律へこの写像を施せば、$F_S$ に対する同じ恒等式を得る。準同型の恒等式にも同じ議論を適用できる。$[n]_F$ は $F$、形式逆元、反復合成だけから一意に構成されるので、その係数変更は $[n]_{F_S}$ に一致する。

$F(X,Y)=X+Y+H(X,Y)$ と書く。$H$ の各単項式は $X$ と $Y$ を含み、全次数は2以上である。
$$ i_F(X)=b_1X+b_2X^2+b_3X^3+\cdots $$
とおき、$F(X,i_F(X))=0$ の係数を次数順に決める。一次の係数から $1+b_1=0$、従って $b_1=-1$ である。
$b_1,\ldots,b_{n-1}$ が一意に決まったとする。$X^n$ の係数において $b_n$ は $Y$ の一次項から係数1で一度だけ現れる。$H(X,i_F(X))$ の $X^n$ の係数には $b_n$ は現れず、$b_1,\ldots,b_{n-1}$ だけで決まる。実際、$H$ の各項は $X^iY^j$ $(i,j\geq1)$ の形なので、$Y^j$ から $b_n$ を使えば次数は少なくとも $i+n>n$ になる。従って $X^n$ の係数を0とする条件が $b_n$ をただ一つ決める。帰納法により右逆元が一意に存在する。
$j_F(X)$ を同じ方法で構成した左逆元、すなわち $F(j_F(X),X)=0$ を満たす唯一の冪級数とする。結合律から
$$ F(j_F(X),F(X,i_F(X)))=F(F(j_F(X),X),i_F(X)) $$
である。左辺は $F(j_F(X),0)=j_F(X)$、右辺は $F(0,i_F(X))=i_F(X)$ なので $j_F=i_F$ である。よって同じ冪級数が左右の逆元である。

準同型性と $F(X,i_F(X))=0$ から
$$ G(f(X),f(i_F(X)))=f(F(X,i_F(X)))=f(0)=0 $$
を得る。一方、$i_G(f(X))$ も $f(X)$ の $G$ に関する逆元である。形式逆元の一意性により両者は等しい。

$f+_Gg$ が準同型であることは
$$ \begin{aligned} (f+_Gg)(F(X,Y)) &=G(G(f(X),f(Y)),G(g(X),g(Y)))\\ &=G(G(f(X),g(X)),G(f(Y),g(Y))) \end{aligned} $$
から従う。二つ目の等号では $G$ の結合律と可換律を使った。零冪級数が加法単位元であり、$f$ の加法逆元は $i_G\circ f$ である。ここで、可換性と結合律により
$$ G\bigl(G(U,V),G(i_G(U),i_G(V))\bigr) =G\bigl(G(U,i_G(U)),G(V,i_G(V))\bigr)=0 $$
である。従って逆元の一意性から
$$ i_G(G(U,V))=G(i_G(U),i_G(V)) $$
を得る。これを $U=f(X)$、$V=f(Y)$ に適用すれば
$$ (i_G\circ f)(F(X,Y)) =G((i_G\circ f)(X),(i_G\circ f)(Y)) $$
となり、$i_G\circ f$ も $F$ から $G$ への準同型である。
$F=G$ とする。合成の結合律は冪級数の合成から従い、乗法単位元は $X$ である。$h,f,g\in\operatorname{End}(F)$ に対して
$$ h\circ(f+_Fg)=h(F(f,g))=F(h\circ f,h\circ g) $$
および
$$ (f+_Fg)\circ h=F(f\circ h,g\circ h) $$
が成り立つので左右の分配律を得る。

まず $m,n\geq0$ とする。$n$ に関する帰納法を用いる。$n=0$ では単位律そのものである。$n$ について成り立つと仮定すれば、結合律により
$$ \begin{aligned} [m+n+1]_F &=F([m+n]_F,X)\\ &=F(F([m]_F,[n]_F),X)\\ &=F([m]_F,[n+1]_F) \end{aligned} $$
を得る。負の整数を含む場合は形式逆元と準同型が逆元に両立することを使えば同じ式へ帰着する。
特に $[n]_F(F(X,Y))$ は、$F(X,Y)$ を $n$ 回 $F$ で加えたものである。結合律と可換律により $X$ の $n$ 個のコピーと $Y$ の $n$ 個のコピーを並べ替えられるので
$$ [n]_F(F(X,Y))=F([n]_F(X),[n]_F(Y)) $$
となり、$[n]_F$ は自己準同型である。一次項については $[n+1]_F=F([n]_F,X)$ と一次項の形から帰納的に $(n+1)X$ を得る。負の $n$ では $i_F(X)=-X+$（2次以上の項）を使う。

まず
$$ a_F(X):=\frac{\partial F}{\partial Y}(X,0) $$
とおく。$F(X,Y)=X+Y+$（2次以上の項）より $a_F(0)=1$ なので、$a_F(X)$ は $R[\![X]\!]$ の可逆元である。結合律
$$ F(F(X,Y),Z)=F(X,F(Y,Z)) $$
を $Z$ で形式微分して $Z=0$ とおくと
$$ a_F(F(X,Y)) =\frac{\partial F}{\partial Y}(X,Y)a_F(Y) $$
を得る。$R$ は $\mathbb Q$-代数なので、冪級数 $a_F(X)^{-1}$ を項別積分できる。定数項を $0$ として
$$ \ell_F(X):=\int_0^X\frac{dT}{a_F(T)} $$
と定める。$a_F(0)=1$ だから $\ell_F(X)=X+$（2次以上の項）である。
ここで
$$ D(X,Y):=\ell_F(F(X,Y))-\ell_F(X)-\ell_F(Y) $$
とおく。$Y$ による形式微分と先の恒等式から
$$ \frac{\partial D}{\partial Y} =\frac{1}{a_F(F(X,Y))}\frac{\partial F}{\partial Y}(X,Y) -\frac{1}{a_F(Y)}=0 $$
を得る。$\mathbb Q$-代数上では、$Y$ による形式微分が $0$ の冪級数は $Y$ に依存しない。さらに $D(X,0)=0$ だから $D=0$ である。従って $\ell_F$ は $F$ から加法形式群への厳密同型である。
一意性を示す。$h(X)=X+$（2次以上の項）が $h(F(X,Y))=h(X)+h(Y)$ を満たすとする。この等式を $Y$ で微分して $Y=0$ とおけば
$$ h'(X)a_F(X)=h'(0)=1 $$
である。従って $h'(X)=a_F(X)^{-1}=\ell_F'(X)$ であり、両者の定数項はともに $0$ なので $h=\ell_F$ となる。