theorem :: QUATERN3:66
for z1, z2, z3, z4 being Quaternion holds ((z1 - z2) - z3) * z4 = ((z1 * z4) - (z2 * z4)) - (z3 * z4)