Theorem IL-4. A single axiom schema for inverse loops. The schema

x · ((((x · y′) · y)′ · z) · ((α · u)′ · (β · u))) = z

can be used to construct a single axiom for any finitely defined equational subvariety of inverse loops.

Proof . First, the equations Σ that specify the subvariety can be bundled together into an equivalent (modulo inverse loops) single equation δ = γ; see [?, ?, ?] for the method. Second, δ = γ is transformed to the equivalent (modulo inverse loops) formula δ_{1}γ′_{1} = δ_{2}γ′_{2}, in which the two sides share no variables and are unifiable; call this equation α = β. Third, α and β are plugged into the axiom. The terms α and β are unifiable without instantiating anything else in the axiom, so by Lem. IL-2, we can derive a basis for inverse loops. Given the basis for inverse loops, by Lem. IL-3, we can derive α = β, so we have the theory of the subvariety and nothing more.