let V be ComplexLinearSpace; :: thesis: for v being VECTOR of V
for z being Complex holds z * (- v) = (- z) * v
let v be VECTOR of V; :: thesis: for z being Complex holds z * (- v) = (- z) * v
let z be Complex; :: thesis: z * (- v) = (- z) * v
thus z * (- v) = z * ((- 1r) * v) by Th4
.= (z * (- 1r)) * v by Def4
.= (- z) * v ; :: thesis: verum