theorem Th45: :: COMPLEX2:47
for x, y, z being Complex holds x .|. (y - z) = (x .|. y) - (x .|. z)