let V be Z_Module; :: thesis: for a being Element of INT.Ring
for v, w being Vector of V holds a * (v - w) = (a * v) - (a * w)
let a be Element of INT.Ring; :: thesis: for v, w being Vector of V holds a * (v - w) = (a * v) - (a * w)
let v, w be Vector of V; :: thesis: a * (v - w) = (a * v) - (a * w)
thus a * (v - w) = (a * v) + (a * (- w)) by VECTSP_1:def 14
.= (a * v) - (a * w) by Th6 ; :: thesis: verum