fof(0, conjecture, ! [Z]: ! [Y]: mult(Z, Y) = mult(Y, Z)).
fof(1, axiom, ! [Y]: mult(e, Y) = Y).
fof(2, axiom, ! [Y]: mult(inverse(Y), Y) = e).
fof(3, axiom, ! [P]: ! [Z]: ! [Y]: mult(mult(P, Z), Y) = mult(P, mult(Z, Y))).
fof(4, axiom, ! [Y]: mult(Y, Y) = e).