let V be Z_Module; :: thesis: for v, u being divisible Vector of V holds v + u is divisible
let v, u be divisible Vector of V; :: thesis: v + u is divisible
thus for a being Element of INT.Ring st a <> 0. INT.Ring holds
ex w being Vector of V st v + u = 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 + u = a * w )
assume A1: a <> 0. INT.Ring ; :: thesis: ex w being Vector of V st v + u = a * w
consider v1 being Vector of V such that
A2: v = a * v1 by A1, defDivisibleVector;
consider u1 being Vector of V such that
A3: u = a * u1 by A1, defDivisibleVector;
take v1 + u1 ; :: thesis: v + u = a * (v1 + u1)
thus v + u = a * (v1 + u1) by A2, A3, VECTSP_1:def 14; :: thesis: verum

end;