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

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