theorem :: CLVECT_1:18

for V being ComplexLinearSpace
for v being VECTOR of V holds Sum <*(- v),(- v)*> = (- (1r + 1r)) * v