let V be free finite-rank Z_Module; :: thesis: for W being Submodule of V holds rank W <= rank V

let W be Submodule of V; :: thesis: rank W <= rank V

consider I being finite Subset of V such that

A1: I is Basis of V by ZMODUL03:def 3;

W is finite-rank ;

then consider A being finite Subset of W such that

A2: A is Basis of W ;

reconsider AA = A as linearly-independent Subset of V by A2, ZMODUL03:15, VECTSP_7:def 3;

card AA c= card I by A1, ZMODUL04:20;

then ( card A c< card I or card A = card I ) ;

then ( card (card A) < card (card I) or card A = card I ) by CARD_2:48;

then card A <= rank V by A1, ZMODUL03:def 5;

hence rank W <= rank V by A2, ZMODUL03:def 5; :: thesis: verum

let W be Submodule of V; :: thesis: rank W <= rank V

consider I being finite Subset of V such that

A1: I is Basis of V by ZMODUL03:def 3;

W is finite-rank ;

then consider A being finite Subset of W such that

A2: A is Basis of W ;

reconsider AA = A as linearly-independent Subset of V by A2, ZMODUL03:15, VECTSP_7:def 3;

card AA c= card I by A1, ZMODUL04:20;

then ( card A c< card I or card A = card I ) ;

then ( card (card A) < card (card I) or card A = card I ) by CARD_2:48;

then card A <= rank V by A1, ZMODUL03:def 5;

hence rank W <= rank V by A2, ZMODUL03:def 5; :: thesis: verum