theorem :: CLVECT_1:15

for V being ComplexLinearSpace
for u, v being VECTOR of V
for z being Complex holds z * (Sum <*v,u*>) = (z * v) + (z * u)