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