let V be Z_Module; :: thesis: 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 )
let W be free Subspace of V; :: thesis: ex A being Subset of V st
( A is Subset of W & A is linearly-independent & Lin A = (Omega). W )
consider AW being Subset of W such that
a1: AW is base by VECTSP_7:def 4;
( 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 Subset of V ;
Lin A = (Omega). W by a1, ZMODUL03:20;
hence ex A being Subset of V st
( A is Subset of W & A is linearly-independent & Lin A = (Omega). W ) by a1, ZMODUL03:15; :: thesis: verum