Theorem RC-3. RC groupoids with identity are associative.

\{ \begin{matrix}RC \\ x · e = x \\ e · x = x \end{matrix} \} ⇒ \{(x · y) · z = x · (y · z)\}.

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

1 x = x 2 x · y = z, u · v = z, w · y = v_{6}, v_{7} · v = v_{6}, x · v_{8} = v_{9},

u · v_{10} = v_{9} → w · v_{8} = v_{7} · v_{10}

3 x · e = x 5 e · x = x 7 (A · B) · C = A · (B · C) → □

8  (x · y) · z = x · (y · z)  [2,3,5,3,1,1,5]
10  □  [8,7]