let V be Z_Module; :: thesis: for v being divisible Vector of V holds - v is divisible
let v be divisible Vector of V; :: thesis: - v is divisible
thus for a being Element of INT.Ring st a <> 0. INT.Ring holds
ex w being Vector of V st - v = a * w :: according to ZMODUL08:def 1 :: thesis: verum

proof

let a be Element of INT.Ring; :: thesis: ( a <> 0. INT.Ring implies ex w being Vector of V st - v = a * w )
assume A1: a <> 0. INT.Ring ; :: thesis: ex w being Vector of V st - v = a * w
consider u being Vector of V such that
A2: v = a * u by A1, defDivisibleVector;
take - u ; :: thesis: - v = a * (- u)
thus - v = a * (- u) by A2, ZMODUL01:6; :: thesis: verum

end;