let V be torsion-free Z_Module; :: thesis: for W1, W2 being free finite-rank Submodule of V ex W3 being free finite-rank Submodule of V st
( rank (W1 + W2) = (rank W1) + (rank W3) & W1 /\ W3 = (0). V & W3 is Submodule of W1 + W2 )
let W1, W2 be free finite-rank Submodule of V; :: thesis: ex W3 being free finite-rank Submodule of V st
( rank (W1 + W2) = (rank W1) + (rank W3) & W1 /\ W3 = (0). V & W3 is Submodule of W1 + W2 )
set I1 = the Basis of W1;
consider I being finite linearly-independent Subset of V such that
A1: ( I is Subset of (W1 + W2) & the Basis of W1 c= I & rank (W1 + W2) = rank (Lin I) ) by LmRankSX2;
set I2 = I \ the Basis of W1;
( the Basis of W1 c= the carrier of W1 & the carrier of W1 c= the carrier of V ) by VECTSP_4:def 2;
then the Basis of W1 c= the carrier of V ;
then reconsider II1 = the Basis of W1 as Subset of V ;
reconsider II1 = II1 as finite Subset of V ;
A10: II1 is linearly-independent by VECTSP_7:def 3, ZMODUL03:15;
reconsider II2 = I \ the Basis of W1 as finite linearly-independent Subset of V by XBOOLE_1:36, ZMODUL02:56;
A3: W1 /\ (Lin II2) = (0). V

proof

B1: (Omega). W1 = Lin the Basis of W1 by VECTSP_7:def 3
.= Lin II1 by ZMODUL03:20 ;
reconsider W1s = (Omega). W1 as free finite-rank Submodule of V by ZMODUL01:42;
(Omega). (Lin II2) = Lin II2 ;
then W1 /\ (Lin II2) = (Lin II1) /\ (Lin II2) by B1, ZMODUL04:23;
hence W1 /\ (Lin II2) = (0). V by A1, A10, ZMODUL06:4; :: thesis: verum

end;

A4: card I = rank (W1 + W2) by A1, ZMODUL05:3;
card II2 = (card I) - (card the Basis of W1) by A1, CARD_2:44
.= (rank (W1 + W2)) - (rank W1) by A4, ZMODUL03:def 5 ;
then A6: rank (Lin II2) = (rank (W1 + W2)) - (rank W1) by ZMODUL05:3;
A11: Lin II2 is Submodule of Lin I by XBOOLE_1:36, ZMODUL02:70;
reconsider II = I as Subset of (W1 + W2) by A1;
Lin II is Submodule of W1 + W2 ;
then A7: Lin I is Submodule of W1 + W2 by ZMODUL03:20;
take Lin II2 ; :: thesis: ( rank (W1 + W2) = (rank W1) + (rank (Lin II2)) & W1 /\ (Lin II2) = (0). V & Lin II2 is Submodule of W1 + W2 )
thus ( rank (W1 + W2) = (rank W1) + (rank (Lin II2)) & W1 /\ (Lin II2) = (0). V & Lin II2 is Submodule of W1 + W2 ) by A3, A6, A7, A11, ZMODUL01:42; :: thesis: verum