Corollary MFL-9. A single axiom for Moufang loops. The axiom schema of Thm. IL-4 gives us a single axiom for the variety of Moufang loops, which is the subvariety of inverse loops satisfying one of the Moufang equations, for example, Moufang-3:

((x · y) · x) · z = x · (y · (x · z)).

We can transform Moufang-3, call it δ = γ, into the appropriate form for the schema by writing it as δ_{1}γ′_{1} = δ_{2}γ′_{2}, in which the two sides of the equation have disjoint sets of variables. When we plug these terms into the schema, we get

x · ((((x · y′) · y)′ · z) · ((
((((x_{1} · y_{1}) · x_{1}) · z_{1}) · (x_{1} · (y_{1} · (x_{1} · z_{1})))′) · u)′ · (
((((x_{2} · y_{2}) · x_{2}) · z_{2}) · (x_{2} · (y_{2} · (x_{2} · z_{2})))′) · u))) = z,

which is a single axiom, in terms of product and inverse, for the variety of Moufang loops.