thus not Cayley-Dickson (Cayley-Dickson (Cayley-Dickson N_Real)) is associative :: thesis: not Cayley-Dickson (Cayley-Dickson (Cayley-Dickson N_Real)) is commutative
proof
take <%<%<%(0. N_Real),(1. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>,<%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>%> ; :: according to GROUP_1:def 3 :: thesis: not for b1, b2 being Element of the carrier of (Cayley-Dickson (Cayley-Dickson (Cayley-Dickson N_Real))) holds (<%<%<%(0. N_Real),(1. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>,<%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>%> * b1) * b2 = <%<%<%(0. N_Real),(1. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>,<%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>%> * (b1 * b2)
take <%<%<%(0. N_Real),(0. N_Real)%>,<%(1. N_Real),(0. N_Real)%>%>,<%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>%> ; :: thesis: not for b1 being Element of the carrier of (Cayley-Dickson (Cayley-Dickson (Cayley-Dickson N_Real))) holds (<%<%<%(0. N_Real),(1. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>,<%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>%> * <%<%<%(0. N_Real),(0. N_Real)%>,<%(1. N_Real),(0. N_Real)%>%>,<%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>%>) * b1 = <%<%<%(0. N_Real),(1. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>,<%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>%> * (<%<%<%(0. N_Real),(0. N_Real)%>,<%(1. N_Real),(0. N_Real)%>%>,<%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>%> * b1)
take <%<%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>,<%<%(0. N_Real),(1. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>%> ; :: thesis: not (<%<%<%(0. N_Real),(1. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>,<%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>%> * <%<%<%(0. N_Real),(0. N_Real)%>,<%(1. N_Real),(0. N_Real)%>%>,<%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>%>) * <%<%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>,<%<%(0. N_Real),(1. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>%> = <%<%<%(0. N_Real),(1. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>,<%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>%> * (<%<%<%(0. N_Real),(0. N_Real)%>,<%(1. N_Real),(0. N_Real)%>%>,<%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>%> * <%<%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>,<%<%(0. N_Real),(1. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>%>)
<%(- (1. N_Real)),(0. N_Real)%> <> <%(1. N_Real),(0. N_Real)%> by Th3;
then <%<%(0. N_Real),(0. N_Real)%>,<%(- (1. N_Real)),(0. N_Real)%>%> <> <%<%(0. N_Real),(0. N_Real)%>,<%(1. N_Real),(0. N_Real)%>%> by Th3;
hence not (<%<%<%(0. N_Real),(1. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>,<%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>%> * <%<%<%(0. N_Real),(0. N_Real)%>,<%(1. N_Real),(0. N_Real)%>%>,<%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>%>) * <%<%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>,<%<%(0. N_Real),(1. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>%> = <%<%<%(0. N_Real),(1. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>,<%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>%> * (<%<%<%(0. N_Real),(0. N_Real)%>,<%(1. N_Real),(0. N_Real)%>%>,<%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>%> * <%<%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>,<%<%(0. N_Real),(1. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>%>) by Th34, Th35, Th3; :: thesis: verum
end;
take <%<%<%(0. N_Real),(1. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>,<%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>%> ; :: according to GROUP_1:def 12 :: thesis: not for b1 being Element of the carrier of (Cayley-Dickson (Cayley-Dickson (Cayley-Dickson N_Real))) holds <%<%<%(0. N_Real),(1. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>,<%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>%> * b1 = b1 * <%<%<%(0. N_Real),(1. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>,<%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>%>
take <%<%<%(0. N_Real),(0. N_Real)%>,<%(1. N_Real),(0. N_Real)%>%>,<%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>%> ; :: thesis: not <%<%<%(0. N_Real),(1. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>,<%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>%> * <%<%<%(0. N_Real),(0. N_Real)%>,<%(1. N_Real),(0. N_Real)%>%>,<%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>%> = <%<%<%(0. N_Real),(0. N_Real)%>,<%(1. N_Real),(0. N_Real)%>%>,<%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>%> * <%<%<%(0. N_Real),(1. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>,<%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>%>
<%(0. N_Real),(1. N_Real)%> <> <%(0. N_Real),(- (1. N_Real))%> by Th3;
then <%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(- (1. N_Real))%>%> <> <%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(1. N_Real)%>%> by Th3;
hence not <%<%<%(0. N_Real),(1. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>,<%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>%> * <%<%<%(0. N_Real),(0. N_Real)%>,<%(1. N_Real),(0. N_Real)%>%>,<%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>%> = <%<%<%(0. N_Real),(0. N_Real)%>,<%(1. N_Real),(0. N_Real)%>%>,<%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>%> * <%<%<%(0. N_Real),(1. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>,<%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>%> by Th32, Th33, Th3; :: thesis: verum