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)
set i = 1. INT.Ring;
thus a * (- v) = (- a) * v by Th5
.= ((- (1. INT.Ring)) * a) * v
.= (- (1. INT.Ring)) * (a * v) by VECTSP_1:def 16
.= - (a * v) by Th2 ; :: thesis: verum