let V be torsion-free Z_Module; 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; 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
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
; ( 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; verum