thus R_Quaternion is add-associative :: thesis: ( R_Quaternion is right_zeroed & R_Quaternion is right_complementable & R_Quaternion is Abelian & R_Quaternion is associative & R_Quaternion is left_unital & R_Quaternion is right_unital & R_Quaternion is distributive & R_Quaternion is almost_right_invertible & not R_Quaternion is degenerated )

proof

let x, y, z be Element of R_Quaternion ; :: according to RLVECT_1:def 6 :: thesis: (x + y) + z = x + (y + z)
reconsider x1 = x, y1 = y, z1 = z as Element of QUATERNION by Def11;
thus (x + y) + z = addquaternion . [(the addF of R_Quaternion . [x1,y1]),z1] by Def11
.= addquaternion . (addquaternion . x1,y1),z1 by Def11
.= addquaternion . (x1 + y1),z1 by Def6
.= (x1 + y1) + z1 by Def6
.= x1 + (y1 + z1) by Th5
.= addquaternion . x1,(y1 + z1) by Def6
.= addquaternion . [x1,(addquaternion . y1,z1)] by Def6
.= addquaternion . [x1,(the addF of R_Quaternion . [y1,z1])] by Def11
.= x + (y + z) by Def11 ; :: thesis: verum

end;

thus R_Quaternion is right_zeroed :: thesis: ( R_Quaternion is right_complementable & R_Quaternion is Abelian & R_Quaternion is associative & R_Quaternion is left_unital & R_Quaternion is right_unital & R_Quaternion is distributive & R_Quaternion is almost_right_invertible & not R_Quaternion is degenerated )

proof

let x be Element of R_Quaternion ; :: according to RLVECT_1:def 7 :: thesis: x + (0. R_Quaternion ) = x
reconsider x1 = x as Element of QUATERNION by Def11;
thus x + (0. R_Quaternion ) = the addF of R_Quaternion . x1,0q by Def11
.= addquaternion . x1,0q by Def11
.= x1 + 0q by Def6
.= x by Th6 ; :: thesis: verum

end;

thus R_Quaternion is right_complementable :: thesis: ( R_Quaternion is Abelian & R_Quaternion is associative & R_Quaternion is left_unital & R_Quaternion is right_unital & R_Quaternion is distributive & R_Quaternion is almost_right_invertible & not R_Quaternion is degenerated )

proof

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

end;

thus R_Quaternion is Abelian :: thesis: ( R_Quaternion is associative & R_Quaternion is left_unital & R_Quaternion is right_unital & R_Quaternion is distributive & R_Quaternion is almost_right_invertible & not R_Quaternion is degenerated )

proof

let x, y be Element of R_Quaternion ; :: according to RLVECT_1:def 5 :: thesis: x + y = y + x
reconsider x1 = x, y1 = y as Element of QUATERNION by Def11;
thus x + y = y + x ; :: thesis: verum

end;

thus R_Quaternion is associative :: thesis: ( R_Quaternion is left_unital & R_Quaternion is right_unital & R_Quaternion is distributive & R_Quaternion is almost_right_invertible & not R_Quaternion is degenerated )

proof

let x, y, z be Element of R_Quaternion ; :: according to GROUP_1:def 4 :: thesis: (x * y) * z = x * (y * z)
reconsider x1 = x, y1 = y, z1 = z as Element of QUATERNION by Def11;
thus (x * y) * z = multquaternion . (the multF of R_Quaternion . x1,y1),z1 by Def11
.= multquaternion . (multquaternion . x1,y1),z1 by Def11
.= multquaternion . (x1 * y1),z1 by Def8
.= (x1 * y1) * z1 by Def8
.= x1 * (y1 * z1) by Th9
.= multquaternion . x1,(y1 * z1) by Def8
.= multquaternion . x1,(multquaternion . y1,z1) by Def8
.= multquaternion . x1,(the multF of R_Quaternion . y1,z1) by Def11
.= x * (y * z) by Def11 ; :: thesis: verum

end;

thus ( R_Quaternion is left_unital & R_Quaternion is right_unital ) ; :: thesis: ( R_Quaternion is distributive & R_Quaternion is almost_right_invertible & not R_Quaternion is degenerated )
thus R_Quaternion is distributive :: thesis: ( R_Quaternion is almost_right_invertible & not R_Quaternion is degenerated )

proof

let x, y, z be Element of R_Quaternion ; :: according to VECTSP_1:def 18 :: thesis: ( x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
reconsider x1 = x, y1 = y, z1 = z as Element of QUATERNION by Def11;
thus x * (y + z) = multquaternion . x1,(the addF of R_Quaternion . y1,z1) by Def11
.= multquaternion . x1,(addquaternion . y1,z1) by Def11
.= multquaternion . x1,(y1 + z1) by Def6
.= x1 * (y1 + z1) by Def8
.= (x1 * y1) + (x1 * z1) by Th10
.= addquaternion . (x1 * y1),(x1 * z1) by Def6
.= addquaternion . (multquaternion . x1,y1),(x1 * z1) by Def8
.= addquaternion . (multquaternion . x1,y1),(multquaternion . x1,z1) by Def8
.= the addF of R_Quaternion . (multquaternion . x1,y1),(multquaternion . x1,z1) by Def11
.= the addF of R_Quaternion . (the multF of R_Quaternion . x1,y1),(multquaternion . x1,z1) by Def11
.= (x * y) + (x * z) by Def11 ; :: thesis: (y + z) * x = (y * x) + (z * x)
thus (y + z) * x = multquaternion . (the addF of R_Quaternion . y1,z1),x1 by Def11
.= multquaternion . (addquaternion . y1,z1),x1 by Def11
.= multquaternion . (y1 + z1),x1 by Def6
.= (y1 + z1) * x1 by Def8
.= (y1 * x1) + (z1 * x1) by Th11
.= addquaternion . (y1 * x1),(z1 * x1) by Def6
.= addquaternion . (multquaternion . y1,x1),(z1 * x1) by Def8
.= addquaternion . (multquaternion . y1,x1),(multquaternion . z1,x1) by Def8
.= the addF of R_Quaternion . (multquaternion . y1,x1),(multquaternion . z1,x1) by Def11
.= the addF of R_Quaternion . (the multF of R_Quaternion . y1,x1),(multquaternion . z1,x1) by Def11
.= (y * x) + (z * x) by Def11 ; :: thesis: verum

end;

thus R_Quaternion is almost_right_invertible :: thesis: not R_Quaternion is degenerated

proof

let x be Element of R_Quaternion ; :: according to ALGSTR_0:def 40 :: thesis: ( x = 0. R_Quaternion or x is right_invertible )
assume A1: x <> 0. R_Quaternion ; :: thesis: x is right_invertible
reconsider x1 = x as Element of QUATERNION by Def11;
reconsider y = x1 " as Element of R_Quaternion by Def11;
take y ; :: according to ALGSTR_0:def 28 :: thesis: x * y = 1. R_Quaternion
A2: x1 <> 0q by A1, Def11;
x * y = 1 by A2, Thaa
.= 1. R_Quaternion by Def11 ;
hence x * y = 1. R_Quaternion ; :: thesis: verum

end;

thus not R_Quaternion is degenerated :: thesis: verum

proof

A: 1. R_Quaternion = 1q by Def11;
0. R_Quaternion <> 1. R_Quaternion by A, Def11;
hence not R_Quaternion is degenerated by STRUCT_0:def 8; :: thesis: verum

end;