for V being RealLinearSpace
for a being Real holds a * (Sum (<*> the carrier of V)) = 0. V by Lm4, Th10;