let z, z1, z2 be quaternion number ; (z - z1) - z2 = (z - z2) - z1
A1:
Im1 ((z - z1) - z2) = (Im1 (z - z1)) - (Im1 z2)
by QUATERNI:42;
A2:
Im1 ((z - z1) - z2) = ((Im1 z) - (Im1 z1)) - (Im1 z2)
by A1, QUATERNI:42;
A3:
Im2 ((z - z1) - z2) = (Im2 (z - z1)) - (Im2 z2)
by QUATERNI:42;
A4:
Im2 ((z - z1) - z2) = ((Im2 z) - (Im2 z1)) - (Im2 z2)
by A3, QUATERNI:42;
A5:
Im2 ((z - z2) - z1) = (Im2 (z - z2)) - (Im2 z1)
by QUATERNI:42;
A6:
Im2 ((z - z2) - z1) = ((Im2 z) - (Im2 z2)) - (Im2 z1)
by A5, QUATERNI:42;
A7:
Im1 ((z - z2) - z1) = (Im1 (z - z2)) - (Im1 z1)
by QUATERNI:42;
A8:
Im1 ((z - z2) - z1) = ((Im1 z) - (Im1 z2)) - (Im1 z1)
by A7, QUATERNI:42;
A9:
Im3 ((z - z2) - z1) = (Im3 (z - z2)) - (Im3 z1)
by QUATERNI:42;
A10:
Im3 ((z - z2) - z1) = ((Im3 z) - (Im3 z2)) - (Im3 z1)
by A9, QUATERNI:42;
A11:
Rea ((z - z2) - z1) = (Rea (z - z2)) - (Rea z1)
by QUATERNI:42;
A12:
Rea ((z - z2) - z1) = ((Rea z) - (Rea z2)) - (Rea z1)
by A11, QUATERNI:42;
A13:
Im3 ((z - z1) - z2) = (Im3 (z - z1)) - (Im3 z2)
by QUATERNI:42;
A14:
Im3 ((z - z1) - z2) = ((Im3 z) - (Im3 z1)) - (Im3 z2)
by A13, QUATERNI:42;
A15:
Rea ((z - z1) - z2) = (Rea (z - z1)) - (Rea z2)
by QUATERNI:42;
A16:
Rea ((z - z1) - z2) = ((Rea z) - (Rea z1)) - (Rea z2)
by A15, QUATERNI:42;
thus
(z - z1) - z2 = (z - z2) - z1
by A16, A2, A4, A14, A12, A8, A6, A10, QUATERNI:25; verum