theorem :: COMPLEX2:40

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