theorem Th57: :: QUATERN3:57

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