Theorem UAL-1. Uniqueness of inversive groupoids under (gL). (Note that the two group operations have the same identity element.)

\{ \begin{matrix}f(e, x) = x, & F (e, x) = x \\ f(x, e) = x, & F (x, e) = x \\ f(g(x), x) = e, & F (G(x), x) = e \\ f(x, g(x)) = e, & F (x, G(x)) = e \end{matrix} \} =(gL)⇒ \{ \begin{matrix}f(x, y) = F (x, y) \\ g(x) = G(x) \end{matrix} \} .

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

2 f(e, x) = x 3 f(x, e) = x 4 f(g(x), x) = e 5 f(x, g(x)) = e 6 F (e, x) = x 7 F (x, e) = x 8 F (G(x), x) = e 9 F (x, G(x)) = e 10 f(A, B) = F (A, B), g(A) = G(A) → □

28,27  f(x, e) = F (e, x)  [3 → 6, flip]
32,31  f(e, x) = F (e, x)  [2 → 6, flip]
40  F (e, x) = F (x, e)  [7 → 6]
41  f(g(F (x, e)), x) = e  [7 → 4]
43  f(g(x), F (x, e)) = e  [7 → 4]
82  f(x, F (e, g(x))) = e  [6 → 5]
94,93  F (x, f(y, g(y))) = x  [5 → 7]
112,111 G(e) = e  [5 → 8 :94]
139,138 G(F (G(x), x)) = e  [8 → 111]
144  F (e, g(e)) = e  [111 → 5 :112,32]
176  F (G(x), x) = F (y, G(y))  [9 → 8]
184,183 F (F (x, G(x)), y) = y  [9 → 6]
186,185 g(e) = e  [9 → 144 :184]
214,213 f(F (G(x), x), y) = F (e, y)  [8 → 31]
231 f(g(F (x, y)), x) = f(g(F (z, y)), z) [41 → 41 :(gL)]
236,235 f(g(F (x, y)), x) = F (e, g(y))  [9 → 231 :184,28, flip]
243 F (e, g(F (x, e))) = F (e, g(x)) [40 → 231 :28,236]
248,247 F (e, g(x)) = F (e, G(x))  [8 → 231 :186,32,236, flip]
268,267 F (x, g(F (y, e))) = F (x, g(y))  [243 :(gL)]
277  f(x, F (e, G(x))) = e  [82 :248]
289  f(g(x), F (x, y)) = f(g(z), F (z, y))  [43 → 43 :(gL)]
291,290 g(x) = F (e, G(x))  [9 → 267 :268,184,248]
292  f(F (e, G(x)), F (x, y)) = f(F (e, G(z)), F (z, y))  [289 :291,291]
311  f(A, B) = F (A, B) → □  [10 :291 :6]
312  f(F (A, e), B) = F (A, B) → □  [7 → 311]
350,349 f(x, G(x)) = e  [9 → 277 :184]

409  f(F (x, G(y)), F (y, z)) = f(F (x, G(u)), F (u, z))  [292 :(gL)]

443,442 f(F (x, G(y)), F (y, z)) = f(F (x, e), F (e, z))

[349 → 409 :350,112, flip]
446,445 f(F (x, e), F (e, y)) = f(F (x, e), y)  [176 → 409 :139,184,443, flip]
449,448 f(F (x, e), y) = F (e, F (x, y))  [176 → 409 :214,443,446, flip]
478  F (e, F (A, B)) = F (A, B) → □  [312 :449]
479  □  [478,6]