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