let c1, c2, c3 be Quaternion; :: thesis: (c1 * c2) * c3 = c1 * (c2 * c3)
consider x1, y1, w1, z1 being Element of REAL such that
A1: c1 = [*x1,y1,w1,z1*] by Lm1;
consider x2, y2, w2, z2 being Element of REAL such that
A2: c2 = [*x2,y2,w2,z2*] by Lm1;
consider x3, y3, w3, z3 being Element of REAL such that
A3: c3 = [*x3,y3,w3,z3*] by Lm1;
A4: (c1 * c2) * c3 = [*((((x1 * x2) - (y1 * y2)) - (w1 * w2)) - (z1 * z2)),((((x1 * y2) + (y1 * x2)) + (w1 * z2)) - (z1 * w2)),((((x1 * w2) + (x2 * w1)) + (y2 * z1)) - (z2 * y1)),((((x1 * z2) + (z1 * x2)) + (y1 * w2)) - (w1 * y2))*] * c3 by A1, A2, QUATERNI:def 10
.= [*((((((((x1 * x2) - (y1 * y2)) - (w1 * w2)) - (z1 * z2)) * x3) - (((((x1 * y2) + (y1 * x2)) + (w1 * z2)) - (z1 * w2)) * y3)) - (((((x1 * w2) + (x2 * w1)) + (y2 * z1)) - (z2 * y1)) * w3)) - (((((x1 * z2) + (z1 * x2)) + (y1 * w2)) - (w1 * y2)) * z3)),((((((((x1 * x2) - (y1 * y2)) - (w1 * w2)) - (z1 * z2)) * y3) + (((((x1 * y2) + (y1 * x2)) + (w1 * z2)) - (z1 * w2)) * x3)) + (((((x1 * w2) + (x2 * w1)) + (y2 * z1)) - (z2 * y1)) * z3)) - (((((x1 * z2) + (z1 * x2)) + (y1 * w2)) - (w1 * y2)) * w3)),((((((((x1 * x2) - (y1 * y2)) - (w1 * w2)) - (z1 * z2)) * w3) + (x3 * ((((x1 * w2) + (x2 * w1)) + (y2 * z1)) - (z2 * y1)))) + (y3 * ((((x1 * z2) + (z1 * x2)) + (y1 * w2)) - (w1 * y2)))) - (z3 * ((((x1 * y2) + (y1 * x2)) + (w1 * z2)) - (z1 * w2)))),((((((((x1 * x2) - (y1 * y2)) - (w1 * w2)) - (z1 * z2)) * z3) + (((((x1 * z2) + (z1 * x2)) + (y1 * w2)) - (w1 * y2)) * x3)) + (((((x1 * y2) + (y1 * x2)) + (w1 * z2)) - (z1 * w2)) * w3)) - (((((x1 * w2) + (x2 * w1)) + (y2 * z1)) - (z2 * y1)) * y3))*] by A3, QUATERNI:def 10
.= [*((((((((x1 * x2) * x3) - ((y1 * y2) * x3)) - ((w1 * w2) * x3)) - ((z1 * z2) * x3)) - (((((x1 * y2) * y3) + ((y1 * x2) * y3)) + ((w1 * z2) * y3)) - ((z1 * w2) * y3))) - (((((x1 * w2) * w3) + ((x2 * w1) * w3)) + ((y2 * z1) * w3)) - ((z2 * y1) * w3))) - (((((x1 * z2) * z3) + ((z1 * x2) * z3)) + ((y1 * w2) * z3)) - ((w1 * y2) * z3))),((((((((x1 * x2) * y3) - ((y1 * y2) * y3)) - ((w1 * w2) * y3)) - ((z1 * z2) * y3)) + (((((x1 * y2) * x3) + ((y1 * x2) * x3)) + ((w1 * z2) * x3)) - ((z1 * w2) * x3))) + (((((x1 * w2) * z3) + ((x2 * w1) * z3)) + ((y2 * z1) * z3)) - ((z2 * y1) * z3))) - (((((x1 * z2) * w3) + ((z1 * x2) * w3)) + ((y1 * w2) * w3)) - ((w1 * y2) * w3))),((((((((x1 * x2) * w3) - ((y1 * y2) * w3)) - ((w1 * w2) * w3)) - ((z1 * z2) * w3)) + (((((x3 * x1) * w2) + ((x3 * x2) * w1)) + ((x3 * y2) * z1)) - ((x3 * z2) * y1))) + (((((y3 * x1) * z2) + ((y3 * z1) * x2)) + ((y3 * y1) * w2)) - ((y3 * w1) * y2))) - (((((z3 * x1) * y2) + ((z3 * y1) * x2)) + ((z3 * w1) * z2)) - ((z3 * z1) * w2))),((((((((x1 * x2) * z3) - ((y1 * y2) * z3)) - ((w1 * w2) * z3)) - ((z1 * z2) * z3)) + (((((x1 * z2) * x3) + ((z1 * x2) * x3)) + ((y1 * w2) * x3)) - ((w1 * y2) * x3))) + (((((x1 * y2) * w3) + ((y1 * x2) * w3)) + ((w1 * z2) * w3)) - ((z1 * w2) * w3))) - (((((x1 * w2) * y3) + ((x2 * w1) * y3)) + ((y2 * z1) * y3)) - ((z2 * y1) * y3)))*] ;
c1 * (c2 * c3) = c1 * [*((((x2 * x3) - (y2 * y3)) - (w2 * w3)) - (z2 * z3)),((((x2 * y3) + (y2 * x3)) + (w2 * z3)) - (z2 * w3)),((((x2 * w3) + (x3 * w2)) + (y3 * z2)) - (z3 * y2)),((((x2 * z3) + (z2 * x3)) + (y2 * w3)) - (w2 * y3))*] by A2, A3, QUATERNI:def 10
.= [*((((x1 * ((((x2 * x3) - (y2 * y3)) - (w2 * w3)) - (z2 * z3))) - (y1 * ((((x2 * y3) + (y2 * x3)) + (w2 * z3)) - (z2 * w3)))) - (w1 * ((((x2 * w3) + (x3 * w2)) + (y3 * z2)) - (z3 * y2)))) - (z1 * ((((x2 * z3) + (z2 * x3)) + (y2 * w3)) - (w2 * y3)))),((((x1 * ((((x2 * y3) + (y2 * x3)) + (w2 * z3)) - (z2 * w3))) + (y1 * ((((x2 * x3) - (y2 * y3)) - (w2 * w3)) - (z2 * z3)))) + (w1 * ((((x2 * z3) + (z2 * x3)) + (y2 * w3)) - (w2 * y3)))) - (z1 * ((((x2 * w3) + (x3 * w2)) + (y3 * z2)) - (z3 * y2)))),((((x1 * ((((x2 * w3) + (x3 * w2)) + (y3 * z2)) - (z3 * y2))) + (((((x2 * x3) - (y2 * y3)) - (w2 * w3)) - (z2 * z3)) * w1)) + (((((x2 * y3) + (y2 * x3)) + (w2 * z3)) - (z2 * w3)) * z1)) - (((((x2 * z3) + (z2 * x3)) + (y2 * w3)) - (w2 * y3)) * y1)),((((x1 * ((((x2 * z3) + (z2 * x3)) + (y2 * w3)) - (w2 * y3))) + (z1 * ((((x2 * x3) - (y2 * y3)) - (w2 * w3)) - (z2 * z3)))) + (y1 * ((((x2 * w3) + (x3 * w2)) + (y3 * z2)) - (z3 * y2)))) - (w1 * ((((x2 * y3) + (y2 * x3)) + (w2 * z3)) - (z2 * w3))))*] by A1, QUATERNI:def 10
.= (c1 * c2) * c3 by A4 ;
hence (c1 * c2) * c3 = c1 * (c2 * c3) ; :: thesis: verum