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

( 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