for V being Z_Module
for W being free finite-rank Subspace of V ex A being finite Subset of V st
( A is finite Subset of W & A is linearly-independent & Lin A = (Omega). W & card A = rank W )