let V be free finite-rank Z_Module; :: thesis: for W being Subspace of V holds W is finite-rank

let W be Subspace of V; :: thesis: W is finite-rank

set A = the Basis of W;

reconsider A0 = the Basis of W as linearly-independent Subset of V by VECTSP_7:def 3, ZMODUL03:15;

A0 is finite by RL5Th25;

hence W is finite-rank by ZMODUL03:def 3; :: thesis: verum

let W be Subspace of V; :: thesis: W is finite-rank

set A = the Basis of W;

reconsider A0 = the Basis of W as linearly-independent Subset of V by VECTSP_7:def 3, ZMODUL03:15;

A0 is finite by RL5Th25;

hence W is finite-rank by ZMODUL03:def 3; :: thesis: verum