theorem :: QUATERNI:57

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