theorem :: QUATERN2:41

(0. R_Quaternion) *' = 0. R_Quaternion