Theorem OC-1. Validity of binary overlay for quasigroups.

\{ \begin{matrix}· is a quasigroup \\ g(x, e) = f(x, e) \\ g(e, x) = f(e, x) \end{matrix} \} =(gL)⇒ \{g(x, y) = f(x, y)\}.

Proof (found by Otter 3.0.4 on gyro at 57.71 seconds).

1 g(A, B) ≠ f(A, B) 6,5 x\(x · y) = y 7 (x/y) · y = x 9 (x · y)/y = x 11 g(x, e) = f(x, e) 12 g(e, x) = f(e, x)

13  (x/y)\x = y  [7 → 5]
17  (x · g(y, e))/f(y, e) = x  [11 → 9]
33  (x · g(e, y))/f(e, y) = x  [12 → 9]
65  (x · g(y, z))/f(y, u) = (x · g(v, z))/f(v, u)  [17 → 17 :(gL) :(gL)]
124  (x · g(y, z))/f(y, z) = x  [65 → 33]
592  g(x, y) = f(x, y)  [124 → 13 :6]
593  □  [592,1]