theorem Th22: :: CSSPACE:27

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