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