theorem Th28: :: CSSPACE:33

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