theorem Th17: :: CLVECT_1:17

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