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) = (- (1r * z)) * v by Th6
.= ((- 1r) * z) * v
.= (- 1r) * (z * v) by Def4
.= - (z * v) by Th3 ; :: thesis: verum