let z1, z2, z be Quaternion; (z - z1) - z2 = (z - z2) - z1
Im1 ((z - z1) - z2) = (Im1 (z - z1)) - (Im1 z2)
by QUATERNI:42;
then A1:
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 A2:
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 A3:
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 A4:
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 A5:
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 A6:
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 A7:
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 A1, A2, A7, A6, A4, A3, A5, QUATERNI:25; verum