theorem :: CLVECT_1:19

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