theorem :: COMPLEX2:35

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