theorem :: QUATERN3:16

for z1, z2 being Quaternion holds (z1 * z2) *' = (z2 *') * (z1 *')