let x, y, z be Complex; :: 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 Def4;
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 Def4;
A7: y1 = y3 by A2, A4, ARYTM_0:10;
A8: y2 = y4 by A2, A4, ARYTM_0:10;
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 Def4;
A12: x1 = x3 by A1, A9, ARYTM_0:10;
A13: x2 = x4 by A1, A9, ARYTM_0:10;
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 Def4;
A17: z1 = z3 by A5, A15, ARYTM_0:10;
A18: z2 = z4 by A5, A15, ARYTM_0:10;
A19: xy1 = + ((* (x1,y1)),(opp (* (x2,y2)))) by A3, A14, ARYTM_0:10;
A20: xy2 = + ((* (x1,y2)),(* (x2,y1))) by A3, A14, ARYTM_0:10;
A21: yz1 = + ((* (y3,z1)),(opp (* (y4,z2)))) by A6, A10, ARYTM_0:10;
A22: yz2 = + ((* (y3,z2)),(* (y4,z1))) by A6, A10, ARYTM_0:10;
+ ((* ((opp x4),(* (y3,z2)))),(* ((opp x4),(* (y4,z1))))) = + ((* ((opp x4),(* (y4,z1)))),(* ((* ((opp x2),y1)),z4))) by A7, A13, A18, ARYTM_0:13
.= + ((* ((* ((opp x2),y2)),z3)),(* ((* ((opp x2),y1)),z4))) by A8, A13, A17, ARYTM_0:13 ;
then A23: + ((* (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:13
.= + ((* ((opp (* (x1,y2))),z4)),(+ ((* ((* ((opp x2),y2)),z3)),(* ((* ((opp x2),y1)),z4))))) by ARYTM_0:15
.= + ((* ((* ((opp x1),y2)),z4)),(+ ((* ((* ((opp x2),y2)),z3)),(* ((* ((opp x2),y1)),z4))))) by ARYTM_0:15
.= + ((* ((* ((opp x2),y2)),z3)),(+ ((* ((* ((opp x1),y2)),z4)),(* ((* ((opp x2),y1)),z4))))) by ARYTM_0:23 ;
A24: + ((* (x3,yz1)),(opp (* (x4,yz2)))) = + ((* (x3,yz1)),(* ((opp x4),yz2))) by ARYTM_0:15
.= + ((* (x3,(+ ((* (y3,z1)),(* ((opp y4),z2)))))),(* ((opp x4),yz2))) by A21, ARYTM_0:15
.= + ((+ ((* (x3,(* (y3,z1)))),(* (x3,(* ((opp y4),z2)))))),(* ((opp x4),(+ ((* (y3,z2)),(* (y4,z1))))))) by A22, ARYTM_0:14
.= + ((+ ((* (x3,(* (y3,z1)))),(* (x3,(* ((opp y4),z2)))))),(+ ((* ((opp x4),(* (y3,z2)))),(* ((opp x4),(* (y4,z1))))))) by ARYTM_0:14
.= + ((* (x3,(* (y3,z1)))),(+ ((* ((* ((opp x2),y2)),z3)),(+ ((* ((* ((opp x1),y2)),z4)),(* ((* ((opp x2),y1)),z4))))))) by A23, ARYTM_0:23
.= + ((+ ((* (x3,(* (y3,z1)))),(* ((* ((opp x2),y2)),z3)))),(+ ((* ((* ((opp x1),y2)),z4)),(* ((* ((opp x2),y1)),z4))))) by ARYTM_0:23
.= + ((+ ((* ((* (x1,y1)),z3)),(* ((* ((opp x2),y2)),z3)))),(+ ((* ((* ((opp x1),y2)),z4)),(* ((* ((opp x2),y1)),z4))))) by A7, A12, A17, ARYTM_0:13
.= + ((* ((+ ((* (x1,y1)),(* ((opp x2),y2)))),z3)),(+ ((* ((* ((opp x1),y2)),z4)),(* ((* ((opp x2),y1)),z4))))) by ARYTM_0:14
.= + ((* ((+ ((* (x1,y1)),(* ((opp x2),y2)))),z3)),(+ ((* ((* ((opp x1),y2)),z4)),(* ((opp (* (x2,y1))),z4))))) by ARYTM_0:15
.= + ((* ((+ ((* (x1,y1)),(* ((opp x2),y2)))),z3)),(+ ((* ((* ((opp x1),y2)),z4)),(opp (* ((* (x2,y1)),z4)))))) by ARYTM_0:15
.= + ((* ((+ ((* (x1,y1)),(* ((opp x2),y2)))),z3)),(+ ((* ((opp (* (x1,y2))),z4)),(opp (* ((* (x2,y1)),z4)))))) by ARYTM_0:15
.= + ((* ((+ ((* (x1,y1)),(* ((opp x2),y2)))),z3)),(+ ((opp (* ((* (x1,y2)),z4))),(opp (* ((* (x2,y1)),z4)))))) by ARYTM_0:15
.= + ((* ((+ ((* (x1,y1)),(* ((opp x2),y2)))),z3)),(opp (+ ((* ((* (x1,y2)),z4)),(* ((* (x2,y1)),z4)))))) by ARYTM_0:25
.= + ((* ((+ ((* (x1,y1)),(* ((opp x2),y2)))),z3)),(opp (* ((+ ((* (x1,y2)),(* (x2,y1)))),z4)))) by ARYTM_0:14
.= + ((* ((+ ((* (x1,y1)),(* ((opp x2),y2)))),z3)),(* ((opp xy2),z4))) by A20, ARYTM_0:15
.= + ((* (xy1,z3)),(* ((opp xy2),z4))) by A19, ARYTM_0:15
.= + ((* (xy1,z3)),(opp (* (xy2,z4)))) by ARYTM_0:15 ;
A25: + ((* ((opp (* (x2,y2))),z4)),(* ((* (x2,y1)),z3))) = + ((opp (* ((* (x2,y2)),z4))),(* ((* (x2,y1)),z3))) by ARYTM_0:15
.= + ((* (x4,(* (y3,z1)))),(opp (* ((* (x2,y2)),z4)))) by A7, A13, A17, ARYTM_0:13
.= + ((* (x4,(* (y3,z1)))),(opp (* (x4,(* (y4,z2)))))) by A8, A13, A18, ARYTM_0:13
.= + ((* (x4,(* (y3,z1)))),(* (x4,(opp (* (y4,z2)))))) by ARYTM_0:15 ;
A26: + ((* ((opp (* (x2,y2))),z4)),(* (xy2,z3))) = + ((* ((opp (* (x2,y2))),z4)),(+ ((* ((* (x1,y2)),z3)),(* ((* (x2,y1)),z3))))) by A20, ARYTM_0:14
.= + ((* ((* (x1,y2)),z3)),(+ ((* ((opp (* (x2,y2))),z4)),(* ((* (x2,y1)),z3))))) by ARYTM_0:23
.= + ((* (x3,(* (y4,z1)))),(+ ((* (x4,(* (y3,z1)))),(* (x4,(opp (* (y4,z2)))))))) by A8, A12, A17, A25, ARYTM_0:13
.= + ((* (x3,(* (y4,z1)))),(* (x4,yz1))) by A21, ARYTM_0:14 ;
+ ((* (xy1,z4)),(* (xy2,z3))) = + ((+ ((* ((* (x1,y1)),z4)),(* ((opp (* (x2,y2))),z4)))),(* (xy2,z3))) by A19, ARYTM_0:14
.= + ((* ((* (x1,y1)),z4)),(+ ((* ((opp (* (x2,y2))),z4)),(* (xy2,z3))))) by ARYTM_0:23
.= + ((* (x3,(* (y3,z2)))),(+ ((* (x3,(* (y4,z1)))),(* (x4,yz1))))) by A7, A12, A18, A26, ARYTM_0:13
.= + ((+ ((* (x3,(* (y3,z2)))),(* (x3,(* (y4,z1)))))),(* (x4,yz1))) by ARYTM_0:23
.= + ((* (x3,yz2)),(* (x4,yz1))) by A22, ARYTM_0:14 ;
hence x * (y * z) = (x * y) * z by A11, A16, A24; :: thesis: verum