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 by A2, A4, ARYTM_0:12;
A8: y2 = y4 by A2, A4, ARYTM_0:12;
consider x3, x4, yz1, yz2 being Element of REAL such that
A9: x = [*x3,x4*] and
A10: y * z = [*yz1,yz2*] and
A11: x * (y * z) = [*(+ (* x3,yz1),(opp (* x4,yz2))),(+ (* x3,yz2),(* x4,yz1))*] by Def5;
A12: x1 = x3 by A1, A9, ARYTM_0:12;
A13: x2 = x4 by A1, A9, ARYTM_0:12;
consider xy1, xy2, z3, z4 being Element of REAL such that
A14: x * y = [*xy1,xy2*] and
A15: z = [*z3,z4*] and
A16: (x * y) * z = [*(+ (* xy1,z3),(opp (* xy2,z4))),(+ (* xy1,z4),(* xy2,z3))*] by Def5;
A17: z1 = z3 by A5, A15, ARYTM_0:12;
A18: z2 = z4 by A5, A15, ARYTM_0:12;
A19: xy1 = + (* x1,y1),(opp (* x2,y2)) by A3, A14, ARYTM_0:12;
A20: xy2 = + (* x1,y2),(* x2,y1) by A3, A14, ARYTM_0:12;
A21: yz1 = + (* y3,z1),(opp (* y4,z2)) by A6, A10, ARYTM_0:12;
A22: yz2 = + (* y3,z2),(* y4,z1) by A6, A10, ARYTM_0:12;
+ (* (opp x4),(* y3,z2)),(* (opp x4),(* y4,z1)) = + (* (opp x4),(* y4,z1)),(* (* (opp x2),y1),z4) by A7, A13, A18, ARYTM_0:15
.= + (* (* (opp x2),y2),z3),(* (* (opp x2),y1),z4) by A8, A13, A17, ARYTM_0:15 ;
then A24: + (* 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 A8, A12, A18, 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 ;
A25: + (* x3,yz1),(opp (* x4,yz2)) = + (* x3,yz1),(* (opp x4),yz2) by ARYTM_0:17
.= + (* x3,(+ (* y3,z1),(* (opp y4),z2))),(* (opp x4),yz2) by A21, ARYTM_0:17
.= + (+ (* x3,(* y3,z1)),(* x3,(* (opp y4),z2))),(* (opp x4),(+ (* y3,z2),(* y4,z1))) by A22, 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 A24, 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, A12, A17, 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 A20, ARYTM_0:17
.= + (* xy1,z3),(* (opp xy2),z4) by A19, ARYTM_0:17
.= + (* xy1,z3),(opp (* xy2,z4)) by ARYTM_0:17 ;
A26: + (* (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, A13, A17, ARYTM_0:15
.= + (* x4,(* y3,z1)),(opp (* x4,(* y4,z2))) by A8, A13, A18, ARYTM_0:15
.= + (* x4,(* y3,z1)),(* x4,(opp (* y4,z2))) by ARYTM_0:17 ;
A27: + (* (opp (* x2,y2)),z4),(* xy2,z3) = + (* (opp (* x2,y2)),z4),(+ (* (* x1,y2),z3),(* (* x2,y1),z3)) by A20, 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 A8, A12, A17, A26, ARYTM_0:15
.= + (* x3,(* y4,z1)),(* x4,yz1) by A21, ARYTM_0:16 ;
+ (* xy1,z4),(* xy2,z3) = + (+ (* (* x1,y1),z4),(* (opp (* x2,y2)),z4)),(* xy2,z3) by A19, 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, A12, A18, A27, ARYTM_0:15
.= + (+ (* x3,(* y3,z2)),(* x3,(* y4,z1))),(* x4,yz1) by ARYTM_0:25
.= + (* x3,yz2),(* x4,yz1) by A22, ARYTM_0:16 ;
hence x * (y * z) = (x * y) * z by A11, A16, A25; :: thesis: verum