let V be Z_Module; :: thesis: for a being Element of INT.Ring
for v being Vector of V holds a * (- v) = (- a) * v
let a be Element of INT.Ring; :: 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. INT.Ring)) * v) by VECTSP_1:14
.= (a * (- (1. INT.Ring))) * v by VECTSP_1:def 16
.= (- a) * v ; :: thesis: verum