let V be free finite-rank Z_Module; :: thesis: for W being Submodule of V
for n being Nat st n <= rank V holds
ex W being strict free Submodule of V st rank W = n
let W be Submodule of V; :: thesis: for n being Nat st n <= rank V holds
ex W being strict free Submodule of V st rank W = n
let n be Nat; :: thesis: ( n <= rank V implies ex W being strict free Submodule of V st rank W = n )
consider I being finite Subset of V such that
A1: I is Basis of V by ZMODUL03:def 3;
assume n <= rank V ; :: thesis: ex W being strict free Submodule of V st rank W = n
then n <= card I by A1, ZMODUL03:def 5;
then consider A being finite Subset of I such that
A2: card A = n by FINSEQ_4:72;
reconsider A = A as finite Subset of V by XBOOLE_1:1;
reconsider W = Lin A as strict free finite-rank Submodule of V ;
A is linearly-independent by ZMODUL02:56, A1, VECTSP_7:def 3;
then rank W = n by A2, RL5Th30;
hence ex W being strict free Submodule of V st rank W = n ; :: thesis: verum