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

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

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

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

11  C · (A · (x · A)) = B · (A · (x · A))  [8 → 6 :7, flip]
13  x′ · (x · (y · x)) = y · x  [4 → 6 :3, flip]
15  (x · y) · x = x · (y · x)  [2 → 6 :3]
29  x′ · (x · x′) = x′  [4 → 15 :3, flip]
60,59  x · x′ = 1  [29 → 13 :5, flip]
68,67  x · 1 = x  [59 → 15 :3,5, flip]
71  (x · y) · y = x · (y · y)  [67 → 6 :3]
95  x · (x′ · x′) = x′  [59 → 71 :3, flip]
121  x · ((x′ · x′) · x) = 1  [95 → 15 :5, flip]
142,141 (x′ · x′) · x = x′  [121 → 13 :68, flip]
143  C = B  [121 → 11 :68,142,60,68]
145  □  [143,10]