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 * (- v) by Th5
.= - (a * v) by Th6 ; :: thesis: verum