theorem :: QUATERN2:41
(0. R_Quaternion) *' = 0. R_Quaternion