theorem :: ZMODUL08:40

for V being free finite-rank Z_Module
for Z being Submodule of DivisibleMod V holds
( Z is finitely-generated iff ex r being non zero Element of F_Rat st Z is Submodule of EMbedding (r,V) )