let c1, c2 be Quaternion; :: thesis:
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: Rea c1 = x1 by A1, QUATERNI:23;
A4: Im1 c1 = y1 by A1, QUATERNI:23;
A5: Im2 c1 = w1 by A1, QUATERNI:23;
A6: Im3 c1 = z1 by A1, QUATERNI:23;
A7: Rea c2 = x2 by A2, QUATERNI:23;
A8: Im1 c2 = y2 by A2, QUATERNI:23;
A9: Im2 c2 = w2 by A2, QUATERNI:23;
A10: Im3 c2 = z2 by A2, QUATERNI:23;
c1 .|. c2 = [*x1,y1,w1,z1*] * [*x2,(- y2),(- w2),(- z2)*] by A1, A2, Th25
.= [*((((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
.= [*(((((Rea c1) * (Rea c2)) + ((Im1 c1) * (Im1 c2))) + ((Im2 c1) * (Im2 c2))) + ((Im3 c1) * (Im3 c2))),(((((Rea c1) * (- (Im1 c2))) + ((Im1 c1) * (Rea c2))) - ((Im2 c1) * (Im3 c2))) + ((Im3 c1) * (Im2 c2))),(((((Rea c1) * (- (Im2 c2))) + ((Rea c2) * (Im2 c1))) - ((Im1 c2) * (Im3 c1))) + ((Im3 c2) * (Im1 c1))),(((((Rea c1) * (- (Im3 c2))) + ((Im3 c1) * (Rea c2))) - ((Im1 c1) * (Im2 c2))) + ((Im2 c1) * (Im1 c2)))*] by A3, A4, A5, A6, A7, A8, A9, A10 ;
hence c1 .|. c2 = [*(((((Rea c1) * (Rea c2)) + ((Im1 c1) * (Im1 c2))) + ((Im2 c1) * (Im2 c2))) + ((Im3 c1) * (Im3 c2))),(((((Rea c1) * (- (Im1 c2))) + ((Im1 c1) * (Rea c2))) - ((Im2 c1) * (Im3 c2))) + ((Im3 c1) * (Im2 c2))),(((((Rea c1) * (- (Im2 c2))) + ((Rea c2) * (Im2 c1))) - ((Im1 c2) * (Im3 c1))) + ((Im3 c2) * (Im1 c1))),(((((Rea c1) * (- (Im3 c2))) + ((Im3 c1) * (Rea c2))) - ((Im1 c1) * (Im2 c2))) + ((Im2 c1) * (Im1 c2)))*] ; :: thesis: