theorem :: QUATERN2:38

1_ R_Quaternion = 1q by Def10;