1q " = 1q by Thd1
.= 1. R_Quaternion by Def11 ;
hence (1. R_Quaternion ) " = 1. R_Quaternion by Def11; :: thesis: verum