let V be torsion-free Z_Module; :: thesis: for W1, W2 being free finite-rank Subspace of V
for I being Basis of W1 st ( for v being Vector of V st v in I holds
(W1 /\ W2) /\ (Lin {v}) <> (0). V ) holds
rank (W1 + W2) = rank W2
defpred S₁[ Nat] means for W1, W2 being free finite-rank Subspace of V
for I being Basis of W1 st ( for v being Vector of V st v in I holds
(W1 /\ W2) /\ (Lin {v}) <> (0). V ) & rank W1 = $1 holds
rank (W1 + W2) = rank W2;
A1: S₁[ 0 ]

proof

let W1, W2 be free finite-rank Subspace of V; :: thesis: for I being Basis of W1 st ( for v being Vector of V st v in I holds
(W1 /\ W2) /\ (Lin {v}) <> (0). V ) & rank W1 = 0 holds
rank (W1 + W2) = rank W2
let I be Basis of W1; :: thesis: ( ( for v being Vector of V st v in I holds
(W1 /\ W2) /\ (Lin {v}) <> (0). V ) & rank W1 = 0 implies rank (W1 + W2) = rank W2 )
assume B1: ( ( for v being Vector of V st v in I holds
(W1 /\ W2) /\ (Lin {v}) <> (0). V ) & rank W1 = 0 ) ; :: thesis: rank (W1 + W2) = rank W2
B2: (Omega). W1 = (0). W1 by B1, ZMODUL05:1
.= (0). V by ZMODUL01:51 ;
reconsider W1s = (Omega). W1, W2s = (Omega). W2 as strict free finite-rank Subspace of V by ZMODUL01:42;
thus rank (W1 + W2) = rank (W1s + W2s) by ZMODUL04:22
.= rank W2s by ZMODUL01:99, B2
.= rank W2 by ZMODUL05:4 ; :: thesis: verum

end;

A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume B1: S₁[n] ; :: thesis: S₁[n + 1]
let W1, W2 be free finite-rank Subspace of V; :: thesis: for I being Basis of W1 st ( for v being Vector of V st v in I holds
(W1 /\ W2) /\ (Lin {v}) <> (0). V ) & rank W1 = n + 1 holds
rank (W1 + W2) = rank W2
let I be Basis of W1; :: thesis: ( ( for v being Vector of V st v in I holds
(W1 /\ W2) /\ (Lin {v}) <> (0). V ) & rank W1 = n + 1 implies rank (W1 + W2) = rank W2 )
assume B2: ( ( for v being Vector of V st v in I holds
(W1 /\ W2) /\ (Lin {v}) <> (0). V ) & rank W1 = n + 1 ) ; :: thesis: rank (W1 + W2) = rank W2
card I > 0 by ZMODUL03:def 5, B2;
then I <> {} the carrier of W1 ;
then consider u being object such that
B3: u in I by XBOOLE_0:7;
reconsider u = u as Vector of W1 by B3;
reconsider uu = u as Vector of V by ZMODUL01:25;
B4: I is linearly-independent by VECTSP_7:def 3;
reconsider II = I as linearly-independent Subset of V by ZMODUL03:15, VECTSP_7:def 3;
I \ {u} is linearly-independent by B4, XBOOLE_1:36, ZMODUL02:56;
then reconsider Iu = I \ {u} as linearly-independent Subset of V by ZMODUL03:15;
BX2X: (Omega). W1 = Lin I by VECTSP_7:def 3
.= Lin II by ZMODUL03:20 ;
then BX2: ( (Omega). W1 = (Lin Iu) + (Lin {uu}) & (Lin Iu) /\ (Lin {uu}) = (0). V & Lin Iu is free & Lin {uu} is free & uu <> 0. V ) by B3, ThLin8;
reconsider LIu = Lin Iu as free finite-rank Subspace of V ;
B5: Iu is Basis of (Lin Iu) by ThLin7;
card Iu = (card I) - (card {u}) by B3, ZFMISC_1:31, CARD_2:44
.= (rank W1) - (card {u}) by ZMODUL03:def 5
.= (n + 1) - 1 by B2, CARD_1:30
.= n ;
then B6: rank LIu = n by B5, ZMODUL03:def 5;
B7X: for v being Vector of V st v in Iu holds
((Lin Iu) /\ W2) /\ (Lin {v}) <> (0). V

proof

let v be Vector of V; :: thesis: ( v in Iu implies ((Lin Iu) /\ W2) /\ (Lin {v}) <> (0). V )
assume C1: v in Iu ; :: thesis: ((Lin Iu) /\ W2) /\ (Lin {v}) <> (0). V
v in I by C1, TARSKI:def 3, XBOOLE_1:36;
then (W1 /\ W2) /\ (Lin {v}) <> (0). V by B2;
then W1 /\ (W2 /\ (Lin {v})) <> (0). V by ZMODUL01:104;
then C2: W2 /\ (Lin {v}) <> (0). V by ZMODUL01:107;
C3: v <> 0. V by C1, ZMODUL02:57;
C4: v in Lin {v} by ZMODUL02:65, ZFMISC_1:31;
v in LIu by C1, ZMODUL02:65;
then LIu /\ (Lin {v}) <> (0). V by C3, ZMODUL02:66, C4, ZMODUL01:94;
hence ((Lin Iu) /\ W2) /\ (Lin {v}) <> (0). V by C2, LmISRank21; :: thesis: verum

end;

(W1 /\ W2) /\ (Lin {uu}) = W1 /\ (W2 /\ (Lin {uu})) by ZMODUL01:104;
then W2 /\ (Lin {uu}) <> (0). V by ZMODUL01:107, B2, B3;
then (LIu + W2) /\ (Lin {uu}) <> (0). V by ThIS1;
then B8: rank ((LIu + W2) + (Lin {uu})) = rank (LIu + W2) by BX2, LmRank2
.= rank W2 by B7X, B1, B5, B6 ;
reconsider W1s = (Omega). W1, W2s = (Omega). W2 as strict free finite-rank Subspace of V by ZMODUL01:42;
B9: (Omega). W1s = W1s ;
(LIu + W2) + (Lin {uu}) = ((Lin {uu}) + LIu) + W2 by ZMODUL01:96
.= W1s + W2 by BX2X, B3, ThLin8
.= W1s + W2s by B9, ZMODUL04:22
.= W1 + W2 by ZMODUL04:22 ;
hence rank (W1 + W2) = rank W2 by B8; :: thesis: verum

end;

A3: for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
let W1, W2 be free finite-rank Subspace of V; :: thesis: for I being Basis of W1 st ( for v being Vector of V st v in I holds
(W1 /\ W2) /\ (Lin {v}) <> (0). V ) holds
rank (W1 + W2) = rank W2
let I be Basis of W1; :: thesis: ( ( for v being Vector of V st v in I holds
(W1 /\ W2) /\ (Lin {v}) <> (0). V ) implies rank (W1 + W2) = rank W2 )
assume A4: for v being Vector of V st v in I holds
(W1 /\ W2) /\ (Lin {v}) <> (0). V ; :: thesis: rank (W1 + W2) = rank W2
set rk = rank W1;
S₁[ rank W1] by A3;
hence rank (W1 + W2) = rank W2 by A4; :: thesis: verum