thus Cayley-Dickson N_Real is associative :: thesis: Cayley-Dickson N_Real is commutative

proof

let x, y, z be Element of (Cayley-Dickson N_Real); :: according to GROUP_1:def 3 :: thesis: (x * y) * z = x * (y * z)
consider x1, x2 being Element of N_Real such that
A1: x = <%x1,x2%> by Th12;
consider y1, y2 being Element of N_Real such that
A2: y = <%y1,y2%> by Th12;
consider z1, z2 being Element of N_Real such that
A3: z = <%z1,z2%> by Th12;
set a1 = (x1 * y1) - ((y2 *') * x2);
set b1 = (x1 * y2) + ((y1 *') * x2);
set a2 = (y1 * z1) - ((z2 *') * y2);
set b2 = (y1 * z2) + ((z1 *') * y2);
A4: y * z = <%((y1 * z1) - ((z2 *') * y2)),((y1 * z2) + ((z1 *') * y2))%> by A2, A3, Def9;
x * y = <%((x1 * y1) - ((y2 *') * x2)),((x1 * y2) + ((y1 *') * x2))%> by A1, A2, Def9;
hence (x * y) * z = <%((((x1 * y1) - ((y2 *') * x2)) * z1) - ((z2 *') * ((x1 * y2) + ((y1 *') * x2)))),((((x1 * y1) - ((y2 *') * x2)) * z2) + ((z1 *') * ((x1 * y2) + ((y1 *') * x2))))%> by A3, Def9
.= <%((x1 * ((y1 * z1) - ((z2 *') * y2))) - ((((y1 * z2) + ((z1 *') * y2)) *') * x2)),((x1 * ((y1 * z2) + ((z1 *') * y2))) + ((((y1 * z1) - ((z2 *') * y2)) *') * x2))%>
.= x * (y * z) by A1, A4, Def9 ;
:: thesis: verum

end;

let x, y be Element of (Cayley-Dickson N_Real); :: according to GROUP_1:def 12 :: thesis: x * y = y * x
consider x1, x2 being Element of N_Real such that
A5: x = <%x1,x2%> by Th12;
consider y1, y2 being Element of N_Real such that
A6: y = <%y1,y2%> by Th12;
thus x * y = <%((x1 * y1) - ((y2 *') * x2)),((x1 * y2) + ((y1 *') * x2))%> by A5, A6, Def9
.= <%((y1 * x1) - ((x2 *') * y2)),((y1 * x2) + ((x1 *') * y2))%>
.= y * x by A5, A6, Def9 ; :: thesis: verum