let V be ComplexLinearSpace; :: thesis: for v, u being VECTOR of V
for z being Complex holds z * (v - u) = (z * v) - (z * u)
let v, u be VECTOR of V; :: thesis: for z being Complex holds z * (v - u) = (z * v) - (z * u)
let z be Complex; :: thesis: z * (v - u) = (z * v) - (z * u)
thus z * (v - u) = (z * v) + (z * (- u)) by Def2
.= (z * v) - (z * u) by Th8 ; :: thesis: verum