(1) |
$\forall \, x, y \in X : f(x, y) \in X$ (D20: Enclosed binary operation)
|
(2) |
$\forall \, x, y \in X : g(x, y) \in X$ (D20: Enclosed binary operation)
|
(3) |
$\forall \, x, y, z \in X : g(x, f(y, z)) = f(g(x, y), g(x, z))$ (D555: Left-distributive binary operation)
|
(4) |
(R3)
$\forall \, x, y, z \in X : g(x, f(y, z)) = f(g(x, y), g(x, z))$ (D555: Left-distributive binary operation)
|
(5) |
$\forall \, x, y, z \in X : f(f(x, y), z) = f(x, f(y, z))$ (D488: Associative binary operation)
|
(6) |
$\forall \, x, y, z \in X : g(g(x, y), z) = g(x, g(y, z))$ (D488: Associative binary operation)
|
(7) |
$\forall \, x, y \in X : f(x, y) = f(y, x)$ (D489: Commutative binary operation)
|
(8) |
$\exists \, 0_R \in X : \forall \, x \in X : f(0_R, x) = f(x, 0_R) = x$ (D39: Identity element)
|
(9) |
$\forall \, x \in X : \exists \, {-x} \in X: f(-x, x) = f(x, -x) = 0_R$ (D40: Inverse element)
|