theorem :: ZMODUL05:9

for V being free finite-rank Z_Module
for n being Nat st rank V < n holds
n Submodules_of V = {}