theorem :: QUATERN3:46
for z1, z2 being quaternion number holds (z1 * z2) " = (z2 ") * (z1 ")