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