theorem Th10: :: CLVECT_1:10
for V being ComplexLinearSpace
for v being VECTOR of V
for z1, z2 being Complex holds (z1 - z2) * v = (z1 * v) - (z2 * v)