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)) * v by Th7
.= z * v ; :: thesis: verum