theorem :: QUATERN2:37
1. R_Quaternion = 1q by Def10;