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

proof

B1: (Omega). W2 = Lin the Basis of W2 by VECTSP_7:def 3
.= Lin I2 by ZMODUL03:20 ;
reconsider W2s = (Omega). W2 as free finite-rank Submodule of V by ZMODUL01:42;
(Omega). (Lin I3) = Lin I3 ;
then B2: W2 /\ (Lin I3) = (Lin I2) /\ (Lin I3) by B1, ZMODUL04:23;
( I2 c= I1 & I3 = I1 \ I2 ) by A1;
hence W2 /\ (Lin I3) = (0). V by B2, ZMODUL06:4; :: thesis: verum

end;

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