set V = Rat-Module ;
for v being Vector of Rat-Module holds v is divisible

proof

let v be Vector of Rat-Module; :: thesis: v is divisible
for a being Element of INT.Ring st a <> 0. INT.Ring holds
ex u being Vector of Rat-Module st a * u = v

proof

let a be Element of INT.Ring; :: thesis: ( a <> 0. INT.Ring implies ex u being Vector of Rat-Module st a * u = v )
assume AS: a <> 0. INT.Ring ; :: thesis: ex u being Vector of Rat-Module st a * u = v
reconsider v1 = v as Element of F_Rat ;
set u1 = (1 / a) * v1;
reconsider u1 = (1 / a) * v1 as Element of F_Rat by RAT_1:def 2;
reconsider u = u1 as Vector of Rat-Module ;
take u ; :: thesis: a * u = v
thus a * u = a * u1 by ZMODUL07:15
.= v by AS, XCMPLX_1:109 ; :: thesis: verum

end;

hence v is divisible ; :: thesis: verum

end;

hence Rat-Module is divisible ; :: thesis: verum