theorem Th48: :: QUATERN2:48

for c1, c2 being Quaternion holds 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)))*]