thus R_Quaternion is add-associative by Th2; :: thesis:
thus R_Quaternion is right_zeroed :: thesis:

proof

let x be Element of R_Quaternion; :: according to RLVECT_1:def 4 :: thesis:
reconsider x1 = x as Element of QUATERNION by Def10;
thus x + (0. R_Quaternion) = the addF of R_Quaternion . (x1,0q) by Def10
.= addquaternion . (x1,0q) by Def10
.= x1 + 0q by Def4
.= x by Th3 ; :: thesis:

end;

thus R_Quaternion is right_complementable :: thesis:

proof

let x be Element of R_Quaternion; :: according to ALGSTR_0:def 16 :: thesis:
reconsider x1 = x as Element of QUATERNION by Def10;
reconsider y = - x1 as Element of R_Quaternion by Def10;
take y ; :: according to ALGSTR_0:def 11 :: thesis:
thus x + y = 0. R_Quaternion by Th39, QUATERNI:def 8; :: thesis:

end;

thus R_Quaternion is Abelian ; :: thesis:
thus R_Quaternion is associative by Th16; :: thesis:
thus ( R_Quaternion is left_unital & R_Quaternion is right_unital ) ; :: thesis:
thus R_Quaternion is distributive by Th17, Th18; :: thesis:
thus R_Quaternion is almost_right_invertible :: thesis:

proof

let x be Element of R_Quaternion; :: according to ALGSTR_0:def 39 :: thesis:
assume A1: x <> 0. R_Quaternion ; :: thesis:
reconsider x1 = x as Element of QUATERNION by Def10;
reconsider y = x1 " as Element of R_Quaternion by Def10;
take y ; :: according to ALGSTR_0:def 28 :: thesis:
x1 <> 0q by A1, Def10;
then x * y = 1 by Th31
.= 1. R_Quaternion by Def10 ;
hence x * y = 1. R_Quaternion ; :: thesis:

end;

1. R_Quaternion = 1q by Def10;
then 0. R_Quaternion <> 1. R_Quaternion by Def10;
hence not R_Quaternion is degenerated ; :: thesis: