theorem :: COMPLEX2:46

for x, y, z being Complex holds (x - y) .|. z = (x .|. z) - (y .|. z) ;