theorem :: QUATERNI:54
for z1, z2 being Quaternion holds (z1 + z2) *' = (z1 *') + (z2 *')