theorem :: ZMODUL06:25

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