let x be Element of R_Quaternion ; :: according to VECTSP_1:def 16 :: thesis: ( x * (1. R_Quaternion ) = x & (1. R_Quaternion ) * x = x )
1. R_Quaternion = 1q by Def10;
hence ( x * (1. R_Quaternion ) = x & (1. R_Quaternion ) * x = x ) by Th14, Th15; :: thesis: verum