let V be Z_Module; :: thesis: 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 )
let W be free finite-rank Subspace of V; :: thesis: 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 )
consider AW being finite Subset of W such that
A1: AW is Basis of W by ZMODUL03:def 3;
A2: ( AW is linearly-independent & Lin AW = (Omega). W ) by A1, VECTSP_7:def 3;
( AW c= the carrier of W & the carrier of W c= the carrier of V ) by VECTSP_4:def 2;
then AW c= the carrier of V ;
then reconsider A = AW as finite Subset of V ;
A3: A is linearly-independent by ZMODUL03:15, A1, VECTSP_7:def 3;
A4: rank W = card A by A1, ZMODUL03:def 5;
Lin A = (Omega). W by A2, ZMODUL03:20;
hence 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 ) by A3, A4; :: thesis: verum