thus for x, y being Element of G_Quaternion holds x + y = y + x ; :: according to RLVECT_1:def 5 :: 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 Th5; :: according to RLVECT_1:def 6 :: 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 7 :: 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 Def13;
thus x + (0. G_Quaternion ) = the addF of G_Quaternion . x1,0q by Def13
.= addquaternion . x1,0q by Def13
.= x1 + 0q by Def6
.= x by Th6 ; :: 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 Def13;
reconsider y = - x1 as Element of G_Quaternion by Def13;
take y ; :: according to ALGSTR_0:def 11 :: thesis: x + y = 0. G_Quaternion
thus x + y = 0. G_Quaternion by Th90, QUATERNI:def 8; :: thesis: verum

end;