for V being ComplexLinearSpace
for z being Complex holds z * (Sum (<*> the carrier of V)) = 0. V by Lm1, Th1;