theorem Th21: :: CSSPACE:26

for X being ComplexUnitarySpace
for x, y, z being Point of X holds (x - y) .|. z = (x .|. z) - (y .|. z)