theorem Th39: :: QUATERN2:39

0. R_Quaternion = 0q by Def10;