Theorem UAL-6. Uniqueness of 5-ary Steiner law under (gL). The type is ⟨5, 5, 0⟩.

\{ \begin{matrix}full symmetry of f \\ f(e, e, e, e, e) = e \\ f(e, e, e, x, f(e, e, e, x, y)) = y \\ full symmetry of g \\ g(e, e, e, e, e) = e \\ g(e, e, e, x, g(e, e, e, x, y)) = y \end{matrix} \} =(gL)⇒ \{g(x, y, z, u, v)=f(x, y, z, u, v)\}.

By Thm. STN-3, we may also assume the universal 5-ary Steiner laws for f and for g:

\begin{matrix}f(u, v, w, x, f(u, v, w, x, y)) = y, \\ g(u, v, w, x, g(u, v, w, x, y)) = y. \end{matrix}

By Lem. UAL-5, we include the equation

f(x_{1}, x_{2}, x_{3}, y, g(x_{4}, x_{5}, x_{6}, y, x_{7})) = f(x_{1}, x_{2}, x_{3}, z, g(x_{4}, x_{5}, x_{6}, z, x_{7})).

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

2 g(x, y, z, u, v) = f(x, y, z, u, v) → g(y, z, u, v, x) = f(y, z, u, v, x) 3 f(e, e, e, e, e) = e 4 f(u, v, w, x, f(u, v, w, x, y)) = y 5 g(e, e, e, e, e) = e 6 g(u, v, w, x, g(u, v, w, x, y)) = y 7 f(x_{1}, x_{2}, x_{3}, y, g(x_{4}, x_{5}, x_{6}, y, x_{7})) = f(x_{1}, x_{2}, x_{3}, z, g(x_{4}, x_{5}, x_{6}, z, x_{7})) 8 g(A, B, C, D, E) = f(A, B, C, D, E) → □

10 f(e, e, e, e, g(e, e, e, e, e)) = e  [5 → 3]
11 f(e, e, e, x, g(e, e, e, x, e)) = e  [7 → 10]
12 g(e, e, e, x, e) = f(e, e, e, x, e)  [11 → 4, flip]
13 g(e, e, x, e, e) = f(e, e, x, e, e)  [2,12]
15 f(e, e, x, e, g(e, e, x, e, e)) = e  [13 → 4]
18 f(e, e, x, y, g(e, e, x, y, e)) = e  [7 → 15]
19 g(e, e, x, y, e) = f(e, e, x, y, e)  [18 → 4, flip]
20 g(e, x, y, e, e) = f(e, x, y, e, e)  [2,19]
22 f(e, x, y, e, g(e, x, y, e, e)) = e  [20 → 4]
25 f(e, x, y, z, g(e, x, y, z, e)) = e  [7 → 22]
26 g(e, x, y, z, e) = f(e, x, y, z, e)  [25 → 4, flip]
27 g(x, y, z, e, e) = f(x, y, z, e, e)  [2,26]
29 f(x, y, z, e, g(x, y, z, e, e)) = e  [27 → 4]
32 f(x, y, z, u, g(x, y, z, u, e)) = e  [7 → 29]
33 g(x, y, z, u, e) = f(x, y, z, u, e)  [32 → 4, flip]
34 g(x, y, z, e, u) = f(x, y, z, e, u)  [2,33]
36 f(x, y, z, e, g(x, y, z, e, u)) = u  [6 → 34, flip]
39 f(x, y, z, u, g(x, y, z, u, v)) = v  [7 → 36]
40 g(x, y, z, u, v) = f(x, y, z, u, v)  [6 → 39, flip]
41 □  [40,8]