theorem :: QUATERN2:26

for c being Quaternion holds (c *') *' = c