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: c2 + c3 = [*(x2 + x3),(y2 + y3),(w2 + w3),(z2 + z3)*] by A2, A3, QUATERNI:def 7;
(c1 + c2) + c3 = [*(x1 + x2),(y1 + y2),(w1 + w2),(z1 + z2)*] + [*x3,y3,w3,z3*] by A1, A2, A3, QUATERNI:def 7
.= [*((x1 + x2) + x3),((y1 + y2) + y3),((w1 + w2) + w3),((z1 + z2) + z3)*] by QUATERNI:def 7
.= [*(x1 + (x2 + x3)),(y1 + (y2 + y3)),(w1 + (w2 + w3)),(z1 + (z2 + z3))*]
.= c1 + (c2 + c3) by A1, A4, QUATERNI:def 7 ;
hence (c1 + c2) + c3 = c1 + (c2 + c3) ; :: thesis: verum