theorem :: RLVECT_1:74

for V being RealLinearSpace
for v being VECTOR of V holds Sum <*v,v,v*> = 3 * v