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