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