theorem :: QUATERN3:15

for z1, z being Quaternion st z is Real holds
(z * z1) *' = (z *') * (z1 *')