theorem :: QUATERN2:46

|.(1. R_Quaternion).| = 1 by Def10, QUATERNI:68;