let x, y, z be complex number ; :: thesis: x * (y * z) = (x * y) * z
consider x1, x2, y1, y2 being Element of REAL such that
A1: x = [*x1,x2*] and
A2: y = [*y1,y2*] and
A3: x * y = [*(+ (* x1,y1),(opp (* x2,y2))),(+ (* x1,y2),(* x2,y1))*] by Def5;
consider y3, y4, z1, z2 being Element of REAL such that
A4: y = [*y3,y4*] and
A5: z = [*z1,z2*] and
A6: y * z = [*(+ (* y3,z1),(opp (* y4,z2))),(+ (* y3,z2),(* y4,z1))*] by Def5;
A7: ( y1 = y3 & y2 = y4 ) by A2, A4, ARYTM_0:12;
consider x3, x4, yz1, yz2 being Element of REAL such that
A8: x = [*x3,x4*] and
A9: y * z = [*yz1,yz2*] and
A10: x * (y * z) = [*(+ (* x3,yz1),(opp (* x4,yz2))),(+ (* x3,yz2),(* x4,yz1))*] by Def5;
A11: ( x1 = x3 & x2 = x4 ) by A1, A8, ARYTM_0:12;
consider xy1, xy2, z3, z4 being Element of REAL such that
A12: x * y = [*xy1,xy2*] and
A13: z = [*z3,z4*] and
A14: (x * y) * z = [*(+ (* xy1,z3),(opp (* xy2,z4))),(+ (* xy1,z4),(* xy2,z3))*] by Def5;
A15: ( z1 = z3 & z2 = z4 ) by A5, A13, ARYTM_0:12;
A16: ( xy1 = + (* x1,y1),(opp (* x2,y2)) & xy2 = + (* x1,y2),(* x2,y1) ) by A3, A12, ARYTM_0:12;
A17: ( yz1 = + (* y3,z1),(opp (* y4,z2)) & yz2 = + (* y3,z2),(* y4,z1) ) by A6, A9, ARYTM_0:12;
+ (* (opp x4),(* y3,z2)),(* (opp x4),(* y4,z1)) = + (* (opp x4),(* y4,z1)),(* (* (opp x2),y1),z4) by A7, A11, A15, ARYTM_0:15
.= + (* (* (opp x2),y2),z3),(* (* (opp x2),y1),z4) by A7, A11, A15, ARYTM_0:15 ;
then A18: + (* x3,(* (opp y4),z2)),(+ (* (opp x4),(* y3,z2)),(* (opp x4),(* y4,z1))) = + (* (* x1,(opp y2)),z4),(+ (* (* (opp x2),y2),z3),(* (* (opp x2),y1),z4)) by A7, A11, A15, ARYTM_0:15
.= + (* (opp (* x1,y2)),z4),(+ (* (* (opp x2),y2),z3),(* (* (opp x2),y1),z4)) by ARYTM_0:17
.= + (* (* (opp x1),y2),z4),(+ (* (* (opp x2),y2),z3),(* (* (opp x2),y1),z4)) by ARYTM_0:17
.= + (* (* (opp x2),y2),z3),(+ (* (* (opp x1),y2),z4),(* (* (opp x2),y1),z4)) by ARYTM_0:25 ;
A19: + (* x3,yz1),(opp (* x4,yz2)) = + (* x3,yz1),(* (opp x4),yz2) by ARYTM_0:17
.= + (* x3,(+ (* y3,z1),(* (opp y4),z2))),(* (opp x4),yz2) by A17, ARYTM_0:17
.= + (+ (* x3,(* y3,z1)),(* x3,(* (opp y4),z2))),(* (opp x4),(+ (* y3,z2),(* y4,z1))) by A17, ARYTM_0:16
.= + (+ (* x3,(* y3,z1)),(* x3,(* (opp y4),z2))),(+ (* (opp x4),(* y3,z2)),(* (opp x4),(* y4,z1))) by ARYTM_0:16
.= + (* x3,(* y3,z1)),(+ (* (* (opp x2),y2),z3),(+ (* (* (opp x1),y2),z4),(* (* (opp x2),y1),z4))) by A18, ARYTM_0:25
.= + (+ (* x3,(* y3,z1)),(* (* (opp x2),y2),z3)),(+ (* (* (opp x1),y2),z4),(* (* (opp x2),y1),z4)) by ARYTM_0:25
.= + (+ (* (* x1,y1),z3),(* (* (opp x2),y2),z3)),(+ (* (* (opp x1),y2),z4),(* (* (opp x2),y1),z4)) by A7, A11, A15, ARYTM_0:15
.= + (* (+ (* x1,y1),(* (opp x2),y2)),z3),(+ (* (* (opp x1),y2),z4),(* (* (opp x2),y1),z4)) by ARYTM_0:16
.= + (* (+ (* x1,y1),(* (opp x2),y2)),z3),(+ (* (* (opp x1),y2),z4),(* (opp (* x2,y1)),z4)) by ARYTM_0:17
.= + (* (+ (* x1,y1),(* (opp x2),y2)),z3),(+ (* (* (opp x1),y2),z4),(opp (* (* x2,y1),z4))) by ARYTM_0:17
.= + (* (+ (* x1,y1),(* (opp x2),y2)),z3),(+ (* (opp (* x1,y2)),z4),(opp (* (* x2,y1),z4))) by ARYTM_0:17
.= + (* (+ (* x1,y1),(* (opp x2),y2)),z3),(+ (opp (* (* x1,y2),z4)),(opp (* (* x2,y1),z4))) by ARYTM_0:17
.= + (* (+ (* x1,y1),(* (opp x2),y2)),z3),(opp (+ (* (* x1,y2),z4),(* (* x2,y1),z4))) by ARYTM_0:27
.= + (* (+ (* x1,y1),(* (opp x2),y2)),z3),(opp (* (+ (* x1,y2),(* x2,y1)),z4)) by ARYTM_0:16
.= + (* (+ (* x1,y1),(* (opp x2),y2)),z3),(* (opp xy2),z4) by A16, ARYTM_0:17
.= + (* xy1,z3),(* (opp xy2),z4) by A16, ARYTM_0:17
.= + (* xy1,z3),(opp (* xy2,z4)) by ARYTM_0:17 ;
A20: + (* (opp (* x2,y2)),z4),(* (* x2,y1),z3) = + (opp (* (* x2,y2),z4)),(* (* x2,y1),z3) by ARYTM_0:17
.= + (* x4,(* y3,z1)),(opp (* (* x2,y2),z4)) by A7, A11, A15, ARYTM_0:15
.= + (* x4,(* y3,z1)),(opp (* x4,(* y4,z2))) by A7, A11, A15, ARYTM_0:15
.= + (* x4,(* y3,z1)),(* x4,(opp (* y4,z2))) by ARYTM_0:17 ;
A21: + (* (opp (* x2,y2)),z4),(* xy2,z3) = + (* (opp (* x2,y2)),z4),(+ (* (* x1,y2),z3),(* (* x2,y1),z3)) by A16, ARYTM_0:16
.= + (* (* x1,y2),z3),(+ (* (opp (* x2,y2)),z4),(* (* x2,y1),z3)) by ARYTM_0:25
.= + (* x3,(* y4,z1)),(+ (* x4,(* y3,z1)),(* x4,(opp (* y4,z2)))) by A7, A11, A15, A20, ARYTM_0:15
.= + (* x3,(* y4,z1)),(* x4,yz1) by A17, ARYTM_0:16 ;
+ (* xy1,z4),(* xy2,z3) = + (+ (* (* x1,y1),z4),(* (opp (* x2,y2)),z4)),(* xy2,z3) by A16, ARYTM_0:16
.= + (* (* x1,y1),z4),(+ (* (opp (* x2,y2)),z4),(* xy2,z3)) by ARYTM_0:25
.= + (* x3,(* y3,z2)),(+ (* x3,(* y4,z1)),(* x4,yz1)) by A7, A11, A15, A21, ARYTM_0:15
.= + (+ (* x3,(* y3,z2)),(* x3,(* y4,z1))),(* x4,yz1) by ARYTM_0:25
.= + (* x3,yz2),(* x4,yz1) by A17, ARYTM_0:16 ;
hence x * (y * z) = (x * y) * z by A10, A14, A19; :: thesis: verum