for a being Element of INT.Ring st a <> 0 holds
ex u being Vector of V st a * u = 0. V

proof

let a be Element of INT.Ring; :: thesis: ( a <> 0 implies ex u being Vector of V st a * u = 0. V )
assume a <> 0 ; :: thesis: ex u being Vector of V st a * u = 0. V
take 0. V ; :: thesis: a * (0. V) = 0. V
thus a * (0. V) = 0. V by ZMODUL01:1; :: thesis: verum

end;

hence 0. V is divisible ; :: thesis: verum