theorem Th60: :: RLVECT_1:61
for V being RealLinearSpace
for v being VECTOR of V holds Sum <*v,v*> = 2 * v