Theorem MFL-5. Simple basis with Moufang-2 (part 2).

\{ \begin{matrix}1 · x = x \\ x′ · x = 1 \\ Moufang-2 \end{matrix} \} ⇒ \{left cancellation\}.

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

3,2 1 · x = x 5,4 x′ · x = 1 7,6 ((x · y) · z) · y = x · (y · (z · y)) 8 A · C = A · B 10 C ≠ B

13  x′ · (x · (y · x)) = y · x  [4 → 6 :3, flip]
16,15  (x · y) · x = x · (y · x)  [2 → 6 :3]
23  x′ · (x · x′) = x′  [4 → 15 :3, flip]
45  x′ · (x · (x · (y · x))) = x · (y · x)  [15 → 13 :16]
53  x′ · (x · (y · (x · (z · x)))) = y · (x · (z · x))  [6 → 13 :7]
60,59  x · x′ = 1  [23 → 13 :5, flip]
69  x · (y · ((x · y)′ · y)) = y  [59 → 6 :3, flip]
72,71  x · 1 = x  [59 → 15 :3,5, flip]
267  x · ((x · x)′ · x) = 1  [69 → 45 :5, flip]
276,275 (x · x)′ · x = x′  [267 → 13 :72, flip]
294,293 x′ · (x · y) = y  [275 → 53 :60,72,276,60,72]
333  C = B  [8 → 293 :294, flip]
335  □  [333,10]