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