:: deftheorem defines .|. QUATERN2:def 11 :
for x, y being quaternion number holds x .|. y = x * (y *');