1. R_Quaternion = 1r by Def10;
hence (1. R_Quaternion) *' = 1. R_Quaternion by QUATERNI:47; :: thesis: verum