let V be torsion-free Z_Module; :: thesis: for W1, W2 being free finite-rank Submodule of V
for I1 being Basis of W1 ex I being finite linearly-independent Subset of V st
( I is Subset of (W1 + W2) & I1 c= I & rank (W1 + W2) = rank (Lin I) )
let W1, W2 be free finite-rank Submodule of V; :: thesis: for I1 being Basis of W1 ex I being finite linearly-independent Subset of V st
( I is Subset of (W1 + W2) & I1 c= I & rank (W1 + W2) = rank (Lin I) )
let I1 be Basis of W1; :: thesis: ex I being finite linearly-independent Subset of V st
( I is Subset of (W1 + W2) & I1 c= I & rank (W1 + W2) = rank (Lin I) )
A2: W1 is Submodule of W1 + W2 by ZMODUL01:97;
then ( I1 c= the carrier of W1 & the carrier of W1 c= the carrier of (W1 + W2) ) by VECTSP_4:def 2;
then I1 c= the carrier of (W1 + W2) ;
then reconsider II1 = I1 as Subset of (W1 + W2) ;
reconsider II1 = II1 as finite Subset of (W1 + W2) ;
reconsider II1 = II1 as finite linearly-independent Subset of (W1 + W2) by A2, VECTSP_7:def 3, ZMODUL03:15;
consider II being finite linearly-independent Subset of (W1 + W2) such that
A3: ( II1 c= II & rank (W1 + W2) = card II ) by LmRankSX1;
( II c= the carrier of (W1 + W2) & the carrier of (W1 + W2) c= the carrier of V ) by VECTSP_4:def 2;
then reconsider I = II as Subset of V by XBOOLE_1:1;
reconsider I = I as finite linearly-independent Subset of V by ZMODUL03:15;
rank (W1 + W2) = rank (Lin I) by A3, ZMODUL05:3;
hence ex I being finite linearly-independent Subset of V st
( I is Subset of (W1 + W2) & I1 c= I & rank (W1 + W2) = rank (Lin I) ) by A3; :: thesis: verum