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