0. R_Quaternion = 0q by Def10;
hence (0. R_Quaternion) *' = 0. R_Quaternion by QUATERNI:45; :: thesis: verum