theorem :: ZMODUL05:10

for V being free finite-rank Z_Module
for W being Submodule of V
for n being Nat holds n Submodules_of W c= n Submodules_of V