let z, z1, z2 be quaternion number ; (z - z1) - z2 = (z - z2) - z1
Im1 ((z - z1) - z2) = (Im1 (z - z1)) - (Im1 z2)
by QUATERNI:42;
then A2:
Im1 ((z - z1) - z2) = ((Im1 z) - (Im1 z1)) - (Im1 z2)
by QUATERNI:42;
Im2 ((z - z1) - z2) = (Im2 (z - z1)) - (Im2 z2)
by QUATERNI:42;
then A4:
Im2 ((z - z1) - z2) = ((Im2 z) - (Im2 z1)) - (Im2 z2)
by QUATERNI:42;
Im2 ((z - z2) - z1) = (Im2 (z - z2)) - (Im2 z1)
by QUATERNI:42;
then A6:
Im2 ((z - z2) - z1) = ((Im2 z) - (Im2 z2)) - (Im2 z1)
by QUATERNI:42;
Im1 ((z - z2) - z1) = (Im1 (z - z2)) - (Im1 z1)
by QUATERNI:42;
then A8:
Im1 ((z - z2) - z1) = ((Im1 z) - (Im1 z2)) - (Im1 z1)
by QUATERNI:42;
Im3 ((z - z2) - z1) = (Im3 (z - z2)) - (Im3 z1)
by QUATERNI:42;
then A10:
Im3 ((z - z2) - z1) = ((Im3 z) - (Im3 z2)) - (Im3 z1)
by QUATERNI:42;
Rea ((z - z2) - z1) = (Rea (z - z2)) - (Rea z1)
by QUATERNI:42;
then A12:
Rea ((z - z2) - z1) = ((Rea z) - (Rea z2)) - (Rea z1)
by QUATERNI:42;
Im3 ((z - z1) - z2) = (Im3 (z - z1)) - (Im3 z2)
by QUATERNI:42;
then A14:
Im3 ((z - z1) - z2) = ((Im3 z) - (Im3 z1)) - (Im3 z2)
by QUATERNI:42;
Rea ((z - z1) - z2) = (Rea (z - z1)) - (Rea z2)
by QUATERNI:42;
then
Rea ((z - z1) - z2) = ((Rea z) - (Rea z1)) - (Rea z2)
by QUATERNI:42;
hence
(z - z1) - z2 = (z - z2) - z1
by A2, A4, A14, A12, A8, A6, A10, QUATERNI:25; verum