let c1, c2 be Quaternion; :: thesis: c1 * (- c2) = - (c1 * c2)
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;
A3: c1 * (- c2) = [*x1,y1,w1,z1*] * [*(- x2),(- y2),(- w2),(- z2)*] by A1, A2, Th4
.= [*((((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)))*] by 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))*] ;
c1 * c2 = [*((((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))*] by A1, A2, QUATERNI:def 10;
then (c1 * (- c2)) + (c1 * c2) = [*(((((- (x1 * x2)) + (y1 * y2)) + (w1 * w2)) + (z1 * z2)) + ((((x1 * x2) - (y1 * y2)) - (w1 * w2)) - (z1 * z2))),(((((- (x1 * y2)) - (y1 * x2)) - (w1 * z2)) + (z1 * w2)) + ((((x1 * y2) + (y1 * x2)) + (w1 * z2)) - (z1 * w2))),(((((- (x1 * w2)) - (x2 * w1)) - (y2 * z1)) + (z2 * y1)) + ((((x1 * w2) + (x2 * w1)) + (y2 * z1)) - (z2 * y1))),(((((- (x1 * z2)) - (z1 * x2)) - (y1 * w2)) + (w1 * y2)) + ((((x1 * z2) + (z1 * x2)) + (y1 * w2)) - (w1 * y2)))*] by A3, QUATERNI:def 7
.= [*(In (0,REAL)),(In (0,REAL))*] by QUATERNI:91
.= 0 by ARYTM_0:def 5 ;
hence c1 * (- c2) = - (c1 * c2) by QUATERNI:def 8; :: thesis: verum