theorem :: QUATERN2:51

for c1, c2 being Quaternion holds |.(c1 .|. c2).| = |.c1.| * |.c2.|