let z, z1, z2 be quaternion number ; :: thesis: (z - z1) - z2 = (z - z2) - z1
( Rea ((z - z1) - z2) = (Rea (z - z1)) - (Rea z2) & Im1 ((z - z1) - z2) = (Im1 (z - z1)) - (Im1 z2) & Im2 ((z - z1) - z2) = (Im2 (z - z1)) - (Im2 z2) & Im3 ((z - z1) - z2) = (Im3 (z - z1)) - (Im3 z2) ) by QUATERNI:42;
then A1: ( Rea ((z - z1) - z2) = ((Rea z) - (Rea z1)) - (Rea z2) & Im1 ((z - z1) - z2) = ((Im1 z) - (Im1 z1)) - (Im1 z2) & Im2 ((z - z1) - z2) = ((Im2 z) - (Im2 z1)) - (Im2 z2) & Im3 ((z - z1) - z2) = ((Im3 z) - (Im3 z1)) - (Im3 z2) ) by QUATERNI:42;
( Rea ((z - z2) - z1) = (Rea (z - z2)) - (Rea z1) & Im1 ((z - z2) - z1) = (Im1 (z - z2)) - (Im1 z1) & Im2 ((z - z2) - z1) = (Im2 (z - z2)) - (Im2 z1) & Im3 ((z - z2) - z1) = (Im3 (z - z2)) - (Im3 z1) ) by QUATERNI:42;
then ( Rea ((z - z2) - z1) = ((Rea z) - (Rea z2)) - (Rea z1) & Im1 ((z - z2) - z1) = ((Im1 z) - (Im1 z2)) - (Im1 z1) & Im2 ((z - z2) - z1) = ((Im2 z) - (Im2 z2)) - (Im2 z1) & Im3 ((z - z2) - z1) = ((Im3 z) - (Im3 z2)) - (Im3 z1) ) by QUATERNI:42;
hence (z - z1) - z2 = (z - z2) - z1 by A1, QUATERNI:25; :: thesis: verum