Theorem TC-11. TC groupoids with identity are commutative semigroups.

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

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

1 x = x 2 x · y = z, u · v = z, x · w = v_{6}, v_{7} · v = v_{6} → u · w = v_{7} · y 3 B · A = A · B, (A · B) · C = A · (B · C) → □ 4 e · x = x 7,6 x · e = x

8  x · (y · z) = y · (x · z)  [2,4,1,4,1]
9  x · y = y · x  [2,4,6,4,6]
32,31  (x · y) · z = y · (x · z)  [2,6,9,8,9 :7, flip]
45  □  [3 :32 :9,8]