1q " = 1q by Th33
.= 1. R_Quaternion by Def10 ;
hence (1. R_Quaternion) " = 1. R_Quaternion by Def10; :: thesis: verum