theorem Th48: :: COMPLEX2:50
for x, y being Complex holds
( Re (x .|. y) = 0 iff ( Im (x .|. y) = |.x.| * |.y.| or Im (x .|. y) = - (|.x.| * |.y.|) ) )