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