theorem :: QUATERN2:44

|.(0. R_Quaternion).| = 0 by Def10, QUATERNI:65;