thus for x, y being Element of G_Quaternion holds x + y = y + x ; :: according to RLVECT_1:def 2 :: thesis: ( G_Quaternion is add-associative & G_Quaternion is right_zeroed & G_Quaternion is right_complementable )
thus for x, y, z being Element of G_Quaternion holds (x + y) + z = x + (y + z) by Th2; :: according to RLVECT_1:def 3 :: thesis: ( G_Quaternion is right_zeroed & G_Quaternion is right_complementable )
thus for x being Element of G_Quaternion holds x + (0. G_Quaternion) = x :: according to RLVECT_1:def 4 :: thesis: G_Quaternion is right_complementable

proof

let x be Element of G_Quaternion; :: thesis: x + (0. G_Quaternion) = x
reconsider x1 = x as Element of QUATERNION by Def9;
thus x + (0. G_Quaternion) = the addF of G_Quaternion . (x1,0q) by Def9
.= addquaternion . (x1,0q) by Def9
.= x1 + 0q by Def4
.= x by Th3 ; :: thesis: verum

end;

thus G_Quaternion is right_complementable :: thesis: verum

proof

let x be Element of G_Quaternion; :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable
reconsider x1 = x as Element of QUATERNION by Def9;
reconsider y = - x1 as Element of G_Quaternion by Def9;
take y ; :: according to ALGSTR_0:def 11 :: thesis: x + y = 0. G_Quaternion
thus x + y = 0. G_Quaternion by Th35, QUATERNI:def 8; :: thesis: verum

end;