given by the graph of the differential of the generating function, we have automatically that the product, when defined, is associative (it satisfies the SGA equation) and that $G_h^{(m)}$ is formally a Lagrangian submanifold of $\overline{G_h}\times\overline{G_h}\times G$. We still have to check that the space of composable pairs is the right one, i.e., $(g,h)\in G_h^{(2)}$ iff $s(g) = t(h)$. We do that by noticing that all products are of the form $(p_1,\nabla_{p_1} S_h(p_1,p_2,x))\bullet (p_2,\nabla_{p_2} S_h(p_1,p_2,x)) = (\nabla_x S_h(p_1,p_2,x),x)$. Thus the check amounts to see that $$s(p_1,\nabla_{p_1}S_h(p_1,p_2,x))=t(p_2,\nabla_{p_2}S_h(p_1,p_2,x))$$ which can be seen by differentiating the SGA equation with respect to $p_2$, putting $p_2 = 0$ and using the fact that $S_h$ is natural.

It remains still to check the following axioms $$\begin{gathered}
t(gh)=t(g)\quad (1),
\quad 
s(gh)=s(h)\quad (2),
\quad
\epsilon(t(g))g=g\quad (3),
\quad g\epsilon(s(g))=g\quad (4),
\\
s(i(g))=t(g)\quad (5),
\quad
i(g)g=\epsilon(s(g))\quad (6),
\quad
gi(g)=\epsilon(t(g))\quad (7),\end{gathered}$$

Axiom 1 is obtained by differentiating the SGA equation w.r.t. $p_1$, putting $p_1=0$ and using naturality of $S_h$. The Axiom 2 is similar but for replacing $p_1$ by $p_3$. Axiom 3 and Axiom 4 are direct consequences of the naturality. The last three axioms are however a bit more tricky. First let us prove two Lemmas.

\[formaldiffeo\] Denote $F_p(x) = 