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 3 :: thesis: (x + y) + z = x + (y + z)
reconsider x1 = x, y1 = y, z1 = z as Element of QUATERNION by Def10;
thus (x + y) + z = addquaternion . [( the addF of R_Quaternion . [x1,y1]),z1] by Def10
.= addquaternion . ((addquaternion . (x1,y1)),z1) by Def10
.= addquaternion . ((x1 + y1),z1) by Def4
.= (x1 + y1) + z1 by Def4
.= x1 + (y1 + z1) by Th2
.= addquaternion . (x1,(y1 + z1)) by Def4
.= addquaternion . [x1,(addquaternion . (y1,z1))] by Def4
.= addquaternion . [x1,( the addF of R_Quaternion . [y1,z1])] by Def10
.= x + (y + z) by Def10 ; :: 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 4 :: thesis: x + (0. R_Quaternion) = x
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: 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 Def10;
reconsider y = - x1 as Element of R_Quaternion by Def10;
take y ; :: according to ALGSTR_0:def 11 :: thesis: x + y = 0. R_Quaternion
thus x + y = 0. R_Quaternion by Th39, 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 2 :: thesis: x + y = y + x
reconsider x1 = x, y1 = y as Element of QUATERNION by Def10;
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 3 :: thesis: (x * y) * z = x * (y * z)
reconsider x1 = x, y1 = y, z1 = z as Element of QUATERNION by Def10;
thus (x * y) * z = multquaternion . (( the multF of R_Quaternion . (x1,y1)),z1) by Def10
.= multquaternion . ((multquaternion . (x1,y1)),z1) by Def10
.= multquaternion . ((x1 * y1),z1) by Def6
.= (x1 * y1) * z1 by Def6
.= x1 * (y1 * z1) by Th16
.= multquaternion . (x1,(y1 * z1)) by Def6
.= multquaternion . (x1,(multquaternion . (y1,z1))) by Def6
.= multquaternion . (x1,( the multF of R_Quaternion . (y1,z1))) by Def10
.= x * (y * z) by Def10 ; :: 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 7 :: 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 Def10;
thus x * (y + z) = multquaternion . (x1,( the addF of R_Quaternion . (y1,z1))) by Def10
.= multquaternion . (x1,(addquaternion . (y1,z1))) by Def10
.= multquaternion . (x1,(y1 + z1)) by Def4
.= x1 * (y1 + z1) by Def6
.= (x1 * y1) + (x1 * z1) by Th17
.= addquaternion . ((x1 * y1),(x1 * z1)) by Def4
.= addquaternion . ((multquaternion . (x1,y1)),(x1 * z1)) by Def6
.= addquaternion . ((multquaternion . (x1,y1)),(multquaternion . (x1,z1))) by Def6
.= the addF of R_Quaternion . ((multquaternion . (x1,y1)),(multquaternion . (x1,z1))) by Def10
.= the addF of R_Quaternion . (( the multF of R_Quaternion . (x1,y1)),(multquaternion . (x1,z1))) by Def10
.= (x * y) + (x * z) by Def10 ; :: thesis: (y + z) * x = (y * x) + (z * x)
thus (y + z) * x = multquaternion . (( the addF of R_Quaternion . (y1,z1)),x1) by Def10
.= multquaternion . ((addquaternion . (y1,z1)),x1) by Def10
.= multquaternion . ((y1 + z1),x1) by Def4
.= (y1 + z1) * x1 by Def6
.= (y1 * x1) + (z1 * x1) by Th18
.= addquaternion . ((y1 * x1),(z1 * x1)) by Def4
.= addquaternion . ((multquaternion . (y1,x1)),(z1 * x1)) by Def6
.= addquaternion . ((multquaternion . (y1,x1)),(multquaternion . (z1,x1))) by Def6
.= the addF of R_Quaternion . ((multquaternion . (y1,x1)),(multquaternion . (z1,x1))) by Def10
.= the addF of R_Quaternion . (( the multF of R_Quaternion . (y1,x1)),(multquaternion . (z1,x1))) by Def10
.= (y * x) + (z * x) by Def10 ; :: 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 Def10;
reconsider y = x1 " as Element of R_Quaternion by Def10;
take y ; :: according to ALGSTR_0:def 28 :: thesis: x * y = 1. R_Quaternion
x1 <> 0q by A1, Def10;
then x * y = 1 by Th31
.= 1. R_Quaternion by Def10 ;
hence x * y = 1. R_Quaternion ; :: thesis: verum

end;

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