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

proof

let W1, W2 be free finite-rank Subspace of V; :: thesis: for v being Vector of V st rank (W1 /\ W2) = rank W1 & (W1 + W2) /\ (Lin {v}) <> (0). V & rank W1 = 0 holds
W2 /\ (Lin {v}) <> (0). V
let v be Vector of V; :: thesis: ( rank (W1 /\ W2) = rank W1 & (W1 + W2) /\ (Lin {v}) <> (0). V & rank W1 = 0 implies W2 /\ (Lin {v}) <> (0). V )
assume B1: ( rank (W1 /\ W2) = rank W1 & (W1 + W2) /\ (Lin {v}) <> (0). V & rank W1 = 0 ) ; :: thesis: W2 /\ (Lin {v}) <> (0). V
then B2: (Omega). W1 = (0). W1 by ZMODUL05:1
.= (0). V by ZMODUL01:51 ;
reconsider WW2 = (Omega). W2 as strict Subspace of V by ZMODUL01:42;
B3: W1 + W2 = ((0). V) + WW2 by B2, ZMODUL04:22
.= WW2 by ZMODUL01:99 ;
(Omega). (Lin {v}) = Lin {v} ;
hence W2 /\ (Lin {v}) <> (0). V by B3, ZMODUL04:23, B1; :: 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 v being Vector of V st rank (W1 /\ W2) = rank W1 & (W1 + W2) /\ (Lin {v}) <> (0). V & rank W1 = n + 1 holds
W2 /\ (Lin {v}) <> (0). V
let v be Vector of V; :: thesis: ( rank (W1 /\ W2) = rank W1 & (W1 + W2) /\ (Lin {v}) <> (0). V & rank W1 = n + 1 implies W2 /\ (Lin {v}) <> (0). V )
assume B2: ( rank (W1 /\ W2) = rank W1 & (W1 + W2) /\ (Lin {v}) <> (0). V & rank W1 = n + 1 ) ; :: thesis: W2 /\ (Lin {v}) <> (0). V
then consider I being finite Subset of V such that
B3: ( I is finite Subset of W1 & I is linearly-independent & Lin I = (Omega). W1 & card I = n + 1 ) by LmFree2;
BX1: I is Basis of W1

proof

reconsider II = I as Subset of W1 by B3;
(Omega). W1 = Lin II by ZMODUL03:20, B3;
hence I is Basis of W1 by VECTSP_7:def 3, B3, ZMODUL03:16; :: thesis: verum

end;

not I is empty by B3;
then consider u being object such that
B4: u in I by XBOOLE_0:def 1;
reconsider u = u as Vector of V by B4;
B5: ( (Omega). W1 = (Lin (I \ {u})) + (Lin {u}) & u <> 0. V ) by B3, B4, ThLin8;
set Iu = I \ {u};
{u} is Subset of I by B4, SUBSET_1:41;
then B7: card (I \ {u}) = (n + 1) - (card {u}) by B3, CARD_2:44
.= (n + 1) - 1 by CARD_1:30
.= n ;
reconsider Iu = I \ {u} as finite Subset of V ;
B8: Iu is linearly-independent by B3, XBOOLE_1:36, ZMODUL02:56;
reconsider LIu = Lin Iu as strict free finite-rank Subspace of V ;
BX2: Iu is Basis of LIu by B8, ThLin7;
C1: for v being Vector of V st v in I holds
W2 /\ (Lin {v}) <> (0). V

proof

let v be Vector of V; :: thesis: ( v in I implies W2 /\ (Lin {v}) <> (0). V )
assume D1: v in I ; :: thesis: W2 /\ (Lin {v}) <> (0). V
(W1 /\ W2) /\ (Lin {v}) = W1 /\ (W2 /\ (Lin {v})) by ZMODUL01:104;
hence W2 /\ (Lin {v}) <> (0). V by ZMODUL01:107, B2, BX1, D1, LmISRank41; :: thesis: verum

end;

B10: rank (LIu /\ W2) = rank LIu

proof

C2: for v being Vector of V st v in Iu holds
W2 /\ (Lin {v}) <> (0). V by C1, ZFMISC_1:56;
for v being Vector of V st v in Iu holds
(LIu /\ W2) /\ (Lin {v}) <> (0). V

proof

let v be Vector of V; :: thesis: ( v in Iu implies (LIu /\ W2) /\ (Lin {v}) <> (0). V )
assume D1: v in Iu ; :: thesis: (LIu /\ W2) /\ (Lin {v}) <> (0). V
( v in LIu & v in Lin {v} ) by D1, ZMODUL02:65, ZFMISC_1:31;
then D2: v in LIu /\ (Lin {v}) by ZMODUL01:94;
consider iv being Vector of V such that
D3: ( iv in W2 /\ (Lin {v}) & iv <> 0. V ) by ZMODUL04:24, C2, D1;
iv in Lin {v} by D3, ZMODUL01:94;
then consider i being Element of INT.Ring such that
D4: iv = i * v by ThLin1;
D5: iv in LIu /\ (Lin {v}) by D2, D4, ZMODUL01:37;
iv in W2 by D3, ZMODUL01:94;
then W2 /\ (LIu /\ (Lin {v})) <> (0). V by D3, ZMODUL02:66, D5, ZMODUL01:94;
hence (LIu /\ W2) /\ (Lin {v}) <> (0). V by ZMODUL01:104; :: thesis: verum

end;

hence rank (LIu /\ W2) = rank LIu by BX2, ThISRank2; :: thesis: verum

end;

(LIu + W2) /\ (Lin {v}) <> (0). V

proof

assume C1: (LIu + W2) /\ (Lin {v}) = (0). V ; :: thesis: contradiction
reconsider WW1 = (Omega). W1 as strict Subspace of V by ZMODUL01:42;
reconsider WW2 = (Omega). W2 as strict Subspace of V by ZMODUL01:42;
C2: (Omega). (LIu + (Lin {u})) = LIu + (Lin {u}) ;
C3: (LIu + W2) + (Lin {u}) = W2 + (LIu + (Lin {u})) by ZMODUL01:96
.= WW2 + (LIu + (Lin {u})) by C2, ZMODUL04:22
.= WW2 + WW1 by B3, B4, ThLin8
.= W2 + W1 by ZMODUL04:22 ;
then (LIu + W2) /\ (Lin {u}) = (0). V by C1, LmRank421, B2;
then C4: rank ((LIu + W2) + (Lin {u})) = (rank (LIu + W2)) + (rank (Lin {u})) by ThRankDirectSum
.= (rank W2) + (rank (Lin {u})) by B10, ThISRank4
.= (rank W2) + 1 by B5, LmRank0a ;
rank ((LIu + W2) + (Lin {u})) = rank W2 by B2, ThISRank4, C3;
hence contradiction by C4; :: thesis: verum

end;

hence W2 /\ (Lin {v}) <> (0). V by B1, B10, B7, ZMODUL03:def 5, BX2; :: 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 v being Vector of V st rank (W1 /\ W2) = rank W1 & (W1 + W2) /\ (Lin {v}) <> (0). V holds
W2 /\ (Lin {v}) <> (0). V
let v be Vector of V; :: thesis: ( rank (W1 /\ W2) = rank W1 & (W1 + W2) /\ (Lin {v}) <> (0). V implies W2 /\ (Lin {v}) <> (0). V )
assume ( rank (W1 /\ W2) = rank W1 & (W1 + W2) /\ (Lin {v}) <> (0). V ) ; :: thesis: W2 /\ (Lin {v}) <> (0). V
hence W2 /\ (Lin {v}) <> (0). V by A3; :: thesis: verum