theorem :: RLVECT_1:62

for V being RealLinearSpace
for v being VECTOR of V holds Sum <*(- v),(- v)*> = (- 2) * v