theorem Th16: :: CSSPACE:21

for a, b being Complex
for X being ComplexUnitarySpace
for x, y, z being Point of X holds x .|. ((a * y) + (b * z)) = ((a *') * (x .|. y)) + ((b *') * (x .|. z))