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;
- c1 = [*(- x1),(- y1),(- w1),(- z1)*] by A1, Th4;
then (- c1) * (- c2) = [*(- x1),(- y1),(- w1),(- z1)*] * [*(- x2),(- y2),(- w2),(- z2)*] by 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 by A1, A2, QUATERNI:def 10 ;
hence (- c1) * (- c2) = c1 * c2 ; :: thesis: verum