theorem :: QUATERN3:16

for z1, z2 being quaternion number holds (z1 * z2) *' = (z2 *') * (z1 *')