theorem Th32: :: RMOD_4:32

for R being Ring
for V being RightMod of R
for v being Vector of V
for l being Linear_Combination of {v} holds Sum l = v * (l . v)