let a be Integer; :: thesis: for V being Z_Module
for v being VECTOR of V holds a * (- v) = (- a) * v
let V be Z_Module; :: thesis: for v being VECTOR of V holds a * (- v) = (- a) * v
let v be VECTOR of V; :: thesis: a * (- v) = (- a) * v
thus a * (- v) = a * ((- 1) * v) by Th2
.= (a * (- 1)) * v by Def4
.= (- a) * v ; :: thesis: verum