theorem Th9: :: CLVECT_1:9

for V being ComplexLinearSpace
for u, v being VECTOR of V
for z being Complex holds z * (v - u) = (z * v) - (z * u)