let a, b, c be Element of (Cayley-Dickson (Cayley-Dickson N_Real)); :: according to GROUP_1:def 3 :: thesis: (a * b) * c = a * (b * c)
consider a1, b1, a2, b2 being Element of N_Real such that
A1: a = <%<%a1,b1%>,<%a2,b2%>%> by Th13;
consider a3, b3, a4, b4 being Element of N_Real such that
A2: b = <%<%a3,b3%>,<%a4,b4%>%> by Th13;
consider a5, b5, a6, b6 being Element of N_Real such that
A3: c = <%<%a5,b5%>,<%a6,b6%>%> by Th13;
set x1 = (<%a1,b1%> * <%a3,b3%>) - ((<%a4,b4%> *') * <%a2,b2%>);
set x2 = (<%a1,b1%> * <%a4,b4%>) + ((<%a3,b3%> *') * <%a2,b2%>);
set x3 = (<%a3,b3%> * <%a5,b5%>) - ((<%a6,b6%> *') * <%a4,b4%>);
set x4 = (<%a3,b3%> * <%a6,b6%>) + ((<%a5,b5%> *') * <%a4,b4%>);
set x11 = ((a1 * a3) - ((b3 *') * b1)) - (((a4 *') * a2) - ((b2 *') * (- b4)));
set x12 = ((a1 * b3) + ((a3 *') * b1)) - (((a4 *') * b2) + ((a2 *') * (- b4)));
set x21 = ((a1 * a4) - ((b4 *') * b1)) + (((a3 *') * a2) - ((b2 *') * (- b3)));
set x22 = ((a1 * b4) + ((a4 *') * b1)) + (((a3 *') * b2) + ((a2 *') * (- b3)));
set x31 = ((a3 * a5) - ((b5 *') * b3)) - (((a6 *') * a4) - ((b4 *') * (- b6)));
set x32 = ((a3 * b5) + ((a5 *') * b3)) - (((a6 *') * b4) + ((a4 *') * (- b6)));
set x41 = ((a3 * a6) - ((b6 *') * b3)) + (((a5 *') * a4) - ((b4 *') * (- b5)));
set x42 = ((a3 * b6) + ((a6 *') * b3)) + (((a5 *') * b4) + ((a4 *') * (- b5)));
A4: <%a1,b1%> * <%a3,b3%> = <%((a1 * a3) - ((b3 *') * b1)),((a1 * b3) + ((a3 *') * b1))%> by Def9;
A5: <%a4,b4%> *' = <%(a4 *'),(- b4)%> by Def9;
A6: <%(a4 *'),(- b4)%> * <%a2,b2%> = <%(((a4 *') * a2) - ((b2 *') * (- b4))),(((a4 *') * b2) + ((a2 *') * (- b4)))%> by Def9;
A7: (<%a1,b1%> * <%a3,b3%>) - ((<%a4,b4%> *') * <%a2,b2%>) = <%(((a1 * a3) - ((b3 *') * b1)) - (((a4 *') * a2) - ((b2 *') * (- b4)))),(((a1 * b3) + ((a3 *') * b1)) - (((a4 *') * b2) + ((a2 *') * (- b4))))%> by A4, A5, A6, Th28;
A8: <%a1,b1%> * <%a4,b4%> = <%((a1 * a4) - ((b4 *') * b1)),((a1 * b4) + ((a4 *') * b1))%> by Def9;
A9: <%a3,b3%> *' = <%(a3 *'),(- b3)%> by Def9;
A10: <%(a3 *'),(- b3)%> * <%a2,b2%> = <%(((a3 *') * a2) - ((b2 *') * (- b3))),(((a3 *') * b2) + ((a2 *') * (- b3)))%> by Def9;
A11: (<%a1,b1%> * <%a4,b4%>) + ((<%a3,b3%> *') * <%a2,b2%>) = <%(((a1 * a4) - ((b4 *') * b1)) + (((a3 *') * a2) - ((b2 *') * (- b3)))),(((a1 * b4) + ((a4 *') * b1)) + (((a3 *') * b2) + ((a2 *') * (- b3))))%> by A8, A9, A10, Def9;
A12: <%a3,b3%> * <%a5,b5%> = <%((a3 * a5) - ((b5 *') * b3)),((a3 * b5) + ((a5 *') * b3))%> by Def9;
A13: <%a6,b6%> *' = <%(a6 *'),(- b6)%> by Def9;
A14: <%(a6 *'),(- b6)%> * <%a4,b4%> = <%(((a6 *') * a4) - ((b4 *') * (- b6))),(((a6 *') * b4) + ((a4 *') * (- b6)))%> by Def9;
A15: (<%a3,b3%> * <%a5,b5%>) - ((<%a6,b6%> *') * <%a4,b4%>) = <%(((a3 * a5) - ((b5 *') * b3)) - (((a6 *') * a4) - ((b4 *') * (- b6)))),(((a3 * b5) + ((a5 *') * b3)) - (((a6 *') * b4) + ((a4 *') * (- b6))))%> by A12, A13, A14, Th28;
A16: <%a3,b3%> * <%a6,b6%> = <%((a3 * a6) - ((b6 *') * b3)),((a3 * b6) + ((a6 *') * b3))%> by Def9;
A17: <%a5,b5%> *' = <%(a5 *'),(- b5)%> by Def9;
A18: <%(a5 *'),(- b5)%> * <%a4,b4%> = <%(((a5 *') * a4) - ((b4 *') * (- b5))),(((a5 *') * b4) + ((a4 *') * (- b5)))%> by Def9;
A19: (<%a3,b3%> * <%a6,b6%>) + ((<%a5,b5%> *') * <%a4,b4%>) = <%(((a3 * a6) - ((b6 *') * b3)) + (((a5 *') * a4) - ((b4 *') * (- b5)))),(((a3 * b6) + ((a6 *') * b3)) + (((a5 *') * b4) + ((a4 *') * (- b5))))%> by A16, A17, A18, Def9;
A20: <%a1,b1%> * ((<%a3,b3%> * <%a5,b5%>) - ((<%a6,b6%> *') * <%a4,b4%>)) = <%((a1 * (((a3 * a5) - ((b5 *') * b3)) - (((a6 *') * a4) - ((b4 *') * (- b6))))) - (((((a3 * b5) + ((a5 *') * b3)) - (((a6 *') * b4) + ((a4 *') * (- b6)))) *') * b1)),((a1 * (((a3 * b5) + ((a5 *') * b3)) - (((a6 *') * b4) + ((a4 *') * (- b6))))) + (((((a3 * a5) - ((b5 *') * b3)) - (((a6 *') * a4) - ((b4 *') * (- b6)))) *') * b1))%> by A15, Def9;
((<%a3,b3%> * <%a6,b6%>) + ((<%a5,b5%> *') * <%a4,b4%>)) *' = <%((((a3 * a6) - ((b6 *') * b3)) + (((a5 *') * a4) - ((b4 *') * (- b5)))) *'),(- (((a3 * b6) + ((a6 *') * b3)) + (((a5 *') * b4) + ((a4 *') * (- b5)))))%> by A19, Def9;
then A21: (((<%a3,b3%> * <%a6,b6%>) + ((<%a5,b5%> *') * <%a4,b4%>)) *') * <%a2,b2%> = <%((((((a3 * a6) - ((b6 *') * b3)) + (((a5 *') * a4) - ((b4 *') * (- b5)))) *') * a2) - ((b2 *') * (- (((a3 * b6) + ((a6 *') * b3)) + (((a5 *') * b4) + ((a4 *') * (- b5))))))),((((((a3 * a6) - ((b6 *') * b3)) + (((a5 *') * a4) - ((b4 *') * (- b5)))) *') * b2) + ((a2 *') * (- (((a3 * b6) + ((a6 *') * b3)) + (((a5 *') * b4) + ((a4 *') * (- b5)))))))%> by Def9;
A22: ((<%a1,b1%> * <%a3,b3%>) - ((<%a4,b4%> *') * <%a2,b2%>)) * <%a5,b5%> = <%(((((a1 * a3) - ((b3 *') * b1)) - (((a4 *') * a2) - ((b2 *') * (- b4)))) * a5) - ((b5 *') * (((a1 * b3) + ((a3 *') * b1)) - (((a4 *') * b2) + ((a2 *') * (- b4)))))),(((((a1 * a3) - ((b3 *') * b1)) - (((a4 *') * a2) - ((b2 *') * (- b4)))) * b5) + ((a5 *') * (((a1 * b3) + ((a3 *') * b1)) - (((a4 *') * b2) + ((a2 *') * (- b4))))))%> by A7, Def9;
(<%a6,b6%> *') * ((<%a1,b1%> * <%a4,b4%>) + ((<%a3,b3%> *') * <%a2,b2%>)) = <%(((a6 *') * (((a1 * a4) - ((b4 *') * b1)) + (((a3 *') * a2) - ((b2 *') * (- b3))))) - (((((a1 * b4) + ((a4 *') * b1)) + (((a3 *') * b2) + ((a2 *') * (- b3)))) *') * (- b6))),(((a6 *') * (((a1 * b4) + ((a4 *') * b1)) + (((a3 *') * b2) + ((a2 *') * (- b3))))) + (((((a1 * a4) - ((b4 *') * b1)) + (((a3 *') * a2) - ((b2 *') * (- b3)))) *') * (- b6)))%> by A11, A13, Def9;
then A23: (((<%a1,b1%> * <%a3,b3%>) - ((<%a4,b4%> *') * <%a2,b2%>)) * <%a5,b5%>) - ((<%a6,b6%> *') * ((<%a1,b1%> * <%a4,b4%>) + ((<%a3,b3%> *') * <%a2,b2%>))) = <%((((((a1 * a3) - ((b3 *') * b1)) - (((a4 *') * a2) - ((b2 *') * (- b4)))) * a5) - ((b5 *') * (((a1 * b3) + ((a3 *') * b1)) - (((a4 *') * b2) + ((a2 *') * (- b4)))))) - (((a6 *') * (((a1 * a4) - ((b4 *') * b1)) + (((a3 *') * a2) - ((b2 *') * (- b3))))) - (((((a1 * b4) + ((a4 *') * b1)) + (((a3 *') * b2) + ((a2 *') * (- b3)))) *') * (- b6)))),((((((a1 * a3) - ((b3 *') * b1)) - (((a4 *') * a2) - ((b2 *') * (- b4)))) * b5) + ((a5 *') * (((a1 * b3) + ((a3 *') * b1)) - (((a4 *') * b2) + ((a2 *') * (- b4)))))) - (((a6 *') * (((a1 * b4) + ((a4 *') * b1)) + (((a3 *') * b2) + ((a2 *') * (- b3))))) + (((((a1 * a4) - ((b4 *') * b1)) + (((a3 *') * a2) - ((b2 *') * (- b3)))) *') * (- b6))))%> by A22, Th28
.= <%(((a1 * (((a3 * a5) - ((b5 *') * b3)) - (((a6 *') * a4) - ((b4 *') * (- b6))))) - (((((a3 * b5) + ((a5 *') * b3)) - (((a6 *') * b4) + ((a4 *') * (- b6)))) *') * b1)) - ((((((a3 * a6) - ((b6 *') * b3)) + (((a5 *') * a4) - ((b4 *') * (- b5)))) *') * a2) - ((b2 *') * (- (((a3 * b6) + ((a6 *') * b3)) + (((a5 *') * b4) + ((a4 *') * (- b5)))))))),(((a1 * (((a3 * b5) + ((a5 *') * b3)) - (((a6 *') * b4) + ((a4 *') * (- b6))))) + (((((a3 * a5) - ((b5 *') * b3)) - (((a6 *') * a4) - ((b4 *') * (- b6)))) *') * b1)) - ((((((a3 * a6) - ((b6 *') * b3)) + (((a5 *') * a4) - ((b4 *') * (- b5)))) *') * b2) + ((a2 *') * (- (((a3 * b6) + ((a6 *') * b3)) + (((a5 *') * b4) + ((a4 *') * (- b5))))))))%>
.= (<%a1,b1%> * ((<%a3,b3%> * <%a5,b5%>) - ((<%a6,b6%> *') * <%a4,b4%>))) - ((((<%a3,b3%> * <%a6,b6%>) + ((<%a5,b5%> *') * <%a4,b4%>)) *') * <%a2,b2%>) by A20, A21, Th28 ;
A24: <%a1,b1%> * ((<%a3,b3%> * <%a6,b6%>) + ((<%a5,b5%> *') * <%a4,b4%>)) = <%((a1 * (((a3 * a6) - ((b6 *') * b3)) + (((a5 *') * a4) - ((b4 *') * (- b5))))) - (((((a3 * b6) + ((a6 *') * b3)) + (((a5 *') * b4) + ((a4 *') * (- b5)))) *') * b1)),((a1 * (((a3 * b6) + ((a6 *') * b3)) + (((a5 *') * b4) + ((a4 *') * (- b5))))) + (((((a3 * a6) - ((b6 *') * b3)) + (((a5 *') * a4) - ((b4 *') * (- b5)))) *') * b1))%> by A19, Def9;
((<%a3,b3%> * <%a5,b5%>) - ((<%a6,b6%> *') * <%a4,b4%>)) *' = <%((((a3 * a5) - ((b5 *') * b3)) - (((a6 *') * a4) - ((b4 *') * (- b6)))) *'),(- (((a3 * b5) + ((a5 *') * b3)) - (((a6 *') * b4) + ((a4 *') * (- b6)))))%> by A15, Def9;
then A25: (((<%a3,b3%> * <%a5,b5%>) - ((<%a6,b6%> *') * <%a4,b4%>)) *') * <%a2,b2%> = <%((((((a3 * a5) - ((b5 *') * b3)) - (((a6 *') * a4) - ((b4 *') * (- b6)))) *') * a2) - ((b2 *') * (- (((a3 * b5) + ((a5 *') * b3)) - (((a6 *') * b4) + ((a4 *') * (- b6))))))),((((((a3 * a5) - ((b5 *') * b3)) - (((a6 *') * a4) - ((b4 *') * (- b6)))) *') * b2) + ((a2 *') * (- (((a3 * b5) + ((a5 *') * b3)) - (((a6 *') * b4) + ((a4 *') * (- b6)))))))%> by Def9;
A26: ((<%a1,b1%> * <%a3,b3%>) - ((<%a4,b4%> *') * <%a2,b2%>)) * <%a6,b6%> = <%(((((a1 * a3) - ((b3 *') * b1)) - (((a4 *') * a2) - ((b2 *') * (- b4)))) * a6) - ((b6 *') * (((a1 * b3) + ((a3 *') * b1)) - (((a4 *') * b2) + ((a2 *') * (- b4)))))),(((((a1 * a3) - ((b3 *') * b1)) - (((a4 *') * a2) - ((b2 *') * (- b4)))) * b6) + ((a6 *') * (((a1 * b3) + ((a3 *') * b1)) - (((a4 *') * b2) + ((a2 *') * (- b4))))))%> by A7, Def9;
(<%a5,b5%> *') * ((<%a1,b1%> * <%a4,b4%>) + ((<%a3,b3%> *') * <%a2,b2%>)) = <%(((a5 *') * (((a1 * a4) - ((b4 *') * b1)) + (((a3 *') * a2) - ((b2 *') * (- b3))))) - (((((a1 * b4) + ((a4 *') * b1)) + (((a3 *') * b2) + ((a2 *') * (- b3)))) *') * (- b5))),(((a5 *') * (((a1 * b4) + ((a4 *') * b1)) + (((a3 *') * b2) + ((a2 *') * (- b3))))) + (((((a1 * a4) - ((b4 *') * b1)) + (((a3 *') * a2) - ((b2 *') * (- b3)))) *') * (- b5)))%> by A17, A11, Def9;
then A27: (((<%a1,b1%> * <%a3,b3%>) - ((<%a4,b4%> *') * <%a2,b2%>)) * <%a6,b6%>) + ((<%a5,b5%> *') * ((<%a1,b1%> * <%a4,b4%>) + ((<%a3,b3%> *') * <%a2,b2%>))) = <%((((((a1 * a3) - ((b3 *') * b1)) - (((a4 *') * a2) - ((b2 *') * (- b4)))) * a6) - ((b6 *') * (((a1 * b3) + ((a3 *') * b1)) - (((a4 *') * b2) + ((a2 *') * (- b4)))))) + (((a5 *') * (((a1 * a4) - ((b4 *') * b1)) + (((a3 *') * a2) - ((b2 *') * (- b3))))) - (((((a1 * b4) + ((a4 *') * b1)) + (((a3 *') * b2) + ((a2 *') * (- b3)))) *') * (- b5)))),((((((a1 * a3) - ((b3 *') * b1)) - (((a4 *') * a2) - ((b2 *') * (- b4)))) * b6) + ((a6 *') * (((a1 * b3) + ((a3 *') * b1)) - (((a4 *') * b2) + ((a2 *') * (- b4)))))) + (((a5 *') * (((a1 * b4) + ((a4 *') * b1)) + (((a3 *') * b2) + ((a2 *') * (- b3))))) + (((((a1 * a4) - ((b4 *') * b1)) + (((a3 *') * a2) - ((b2 *') * (- b3)))) *') * (- b5))))%> by A26, Def9
.= <%(((a1 * (((a3 * a6) - ((b6 *') * b3)) + (((a5 *') * a4) - ((b4 *') * (- b5))))) - (((((a3 * b6) + ((a6 *') * b3)) + (((a5 *') * b4) + ((a4 *') * (- b5)))) *') * b1)) + ((((((a3 * a5) - ((b5 *') * b3)) - (((a6 *') * a4) - ((b4 *') * (- b6)))) *') * a2) - ((b2 *') * (- (((a3 * b5) + ((a5 *') * b3)) - (((a6 *') * b4) + ((a4 *') * (- b6)))))))),(((a1 * (((a3 * b6) + ((a6 *') * b3)) + (((a5 *') * b4) + ((a4 *') * (- b5))))) + (((((a3 * a6) - ((b6 *') * b3)) + (((a5 *') * a4) - ((b4 *') * (- b5)))) *') * b1)) + ((((((a3 * a5) - ((b5 *') * b3)) - (((a6 *') * a4) - ((b4 *') * (- b6)))) *') * b2) + ((a2 *') * (- (((a3 * b5) + ((a5 *') * b3)) - (((a6 *') * b4) + ((a4 *') * (- b6))))))))%>
.= (<%a1,b1%> * ((<%a3,b3%> * <%a6,b6%>) + ((<%a5,b5%> *') * <%a4,b4%>))) + ((((<%a3,b3%> * <%a5,b5%>) - ((<%a6,b6%> *') * <%a4,b4%>)) *') * <%a2,b2%>) by A24, A25, Def9 ;
A28: b * c = <%((<%a3,b3%> * <%a5,b5%>) - ((<%a6,b6%> *') * <%a4,b4%>)),((<%a3,b3%> * <%a6,b6%>) + ((<%a5,b5%> *') * <%a4,b4%>))%> by A2, A3, Def9;
a * b = <%((<%a1,b1%> * <%a3,b3%>) - ((<%a4,b4%> *') * <%a2,b2%>)),((<%a1,b1%> * <%a4,b4%>) + ((<%a3,b3%> *') * <%a2,b2%>))%> by A1, A2, Def9;
hence (a * b) * c = <%((((<%a1,b1%> * <%a3,b3%>) - ((<%a4,b4%> *') * <%a2,b2%>)) * <%a5,b5%>) - ((<%a6,b6%> *') * ((<%a1,b1%> * <%a4,b4%>) + ((<%a3,b3%> *') * <%a2,b2%>)))),((((<%a1,b1%> * <%a3,b3%>) - ((<%a4,b4%> *') * <%a2,b2%>)) * <%a6,b6%>) + ((<%a5,b5%> *') * ((<%a1,b1%> * <%a4,b4%>) + ((<%a3,b3%> *') * <%a2,b2%>))))%> by A3, Def9
.= a * (b * c) by A1, A28, A23, A27, Def9 ;
:: thesis: verum