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