:: deftheorem defines .|. COMPLEX2:def 1 :
for x, y being Complex holds x .|. y = x * (y *');