for x, y, z being Element of G_Quaternion holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. G_Quaternion) = x ) by RLVECT_1:def 3, RLVECT_1:def 4;