theorem :: QUATERN3:46

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