theorem Th26: :: CSSPACE:31

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