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