theorem :: QUATERN3:65

for z1, z2, z3, z4 being Quaternion holds ((z1 - z2) + z3) * z4 = ((z1 * z4) - (z2 * z4)) + (z3 * z4)