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

proof

let W be free finite-rank Subspace of V; :: thesis: for v being Vector of V st v <> 0. V & W /\ (Lin {v}) <> (0). V & rank W = 0 + 1 holds
rank (W + (Lin {v})) = rank W
let v be Vector of V; :: thesis: ( v <> 0. V & W /\ (Lin {v}) <> (0). V & rank W = 0 + 1 implies rank (W + (Lin {v})) = rank W )
assume B1: ( v <> 0. V & W /\ (Lin {v}) <> (0). V & rank W = 0 + 1 ) ; :: thesis: rank (W + (Lin {v})) = rank W
consider uu being Vector of W such that
B3: ( uu <> 0. W & (Omega). W = Lin {uu} ) by B1, ZMODUL05:5;
reconsider u = uu as Vector of V by ZMODUL01:25;
B4: u <> 0. V by ZMODUL01:26, B3;
reconsider Ws = (Omega). W as strict Subspace of V by ZMODUL01:42;
reconsider Lv = (Omega). (Lin {v}) as strict Subspace of V ;
B6: (Lin {u}) + (Lin {v}) = Ws + Lv by B3, ZMODUL03:20
.= W + (Lin {v}) by ZMODUL04:22 ;
(Lin {u}) /\ (Lin {v}) = Ws /\ Lv by B3, ZMODUL03:20
.= W /\ (Lin {v}) by ZMODUL04:23 ;
hence rank (W + (Lin {v})) = rank W by B6, B1, B4, LmRank1; :: 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 W be free finite-rank Subspace of V; :: thesis: for v being Vector of V st v <> 0. V & W /\ (Lin {v}) <> (0). V & rank W = (n + 1) + 1 holds
rank (W + (Lin {v})) = rank W
let v be Vector of V; :: thesis: ( v <> 0. V & W /\ (Lin {v}) <> (0). V & rank W = (n + 1) + 1 implies rank (W + (Lin {v})) = rank W )
assume B2: ( v <> 0. V & W /\ (Lin {v}) <> (0). V & rank W = (n + 1) + 1 ) ; :: thesis: rank (W + (Lin {v})) = rank W
consider I being finite Subset of V such that
B3: ( I is finite Subset of W & I is linearly-independent & Lin I = (Omega). W & card I = rank W ) by LmFree2;
I <> {} the carrier of W by B2, B3;
then consider w being object such that
B5: w in I by XBOOLE_0:7;
reconsider w = w as Vector of V by B5;
B6: ( (Omega). W = (Lin (I \ {w})) + (Lin {w}) & (Lin (I \ {w})) /\ (Lin {w}) = (0). V & Lin (I \ {w}) is free & Lin {w} is free & w <> 0. V ) by B3, B5, ThLin8;
reconsider LIw = Lin (I \ {w}), Lw = Lin {w} as free finite-rank Subspace of V ;
B7: card (I \ {w}) = (card I) - (card {w}) by B5, ZFMISC_1:31, CARD_2:44
.= (n + 2) - 1 by CARD_1:30, B2, B3
.= n + 1 ;
reconsider Lv = Lin {v} as free finite-rank Subspace of V ;
I \ {w} is linearly-independent by B3, ZMODUL02:56, XBOOLE_1:36;
then reconsider Iw = I \ {w} as Basis of (Lin (I \ {w})) by ThLin7;
B10: rank (Lin (I \ {w})) = card Iw by ZMODUL03:def 5
.= n + 1 by B7 ;

per cases ( ((Lin (I \ {w})) + (Lin {v})) /\ (Lin {w}) = (0). V or ((Lin (I \ {w})) + (Lin {v})) /\ (Lin {w}) <> (0). V ) ;

suppose C1: ((Lin (I \ {w})) + (Lin {v})) /\ (Lin {w}) = (0). V ; :: thesis: rank (W + (Lin {v})) = rank W

then C2: rank (((Lin (I \ {w})) + (Lin {v})) + (Lin {w})) = (rank ((Lin (I \ {w})) + (Lin {v}))) + (rank (Lin {w})) by ThRankDirectSum;
C3: (Lin (I \ {w})) /\ (Lin {v}) <> (0). V

proof

assume D1: (Lin (I \ {w})) /\ (Lin {v}) = (0). V ; :: thesis: contradiction
consider x being Vector of V such that
D2: ( x in W /\ (Lin {v}) & x <> 0. V ) by B2, ZMODUL04:24;
x in W by D2, ZMODUL01:94;
then x in (Omega). W ;
then consider x1, x2 being Vector of V such that
D3: ( x1 in Lin (I \ {w}) & x2 in Lin {w} & x = x1 + x2 ) by B6, ZMODUL01:92;
D4: x in Lin {v} by D2, ZMODUL01:94;
D5: x - x1 = x2 + (x1 - x1) by RLVECT_1:28, D3
.= x2 + (0. V) by RLVECT_1:15
.= x2 ;
- x1 in Lin (I \ {w}) by D3, ZMODUL01:38;
then D6: x2 in (Lin (I \ {w})) + (Lin {v}) by D4, D5, ZMODUL01:92;
x2 <> 0. V by D1, D2, ZMODUL02:66, D4, ZMODUL01:94, D3;
hence contradiction by C1, D6, ZMODUL02:66, D3, ZMODUL01:94; :: thesis: verum

end;

C4: rank (LIw + (Lin {v})) = n + 1 by B10, B1, B2, C3;
C5: rank ((LIw + (Lin {v})) + (Lin {w})) = (n + 1) + 1 by C2, C4, B6, LmRank0a
.= n + 2 ;
(Omega). (Lin {v}) = Lin {v} ;
then W + (Lin {v}) = ((Lin (I \ {w})) + (Lin {w})) + (Lin {v}) by B6, ZMODUL04:22
.= ((Lin (I \ {w})) + (Lin {v})) + (Lin {w}) by ZMODUL01:96 ;
hence rank (W + (Lin {v})) = rank W by B2, C5; :: thesis: verum

end;

suppose C1: ((Lin (I \ {w})) + (Lin {v})) /\ (Lin {w}) <> (0). V ; :: thesis: rank (W + (Lin {v})) = rank W

per cases ( (Lin {v}) /\ (Lin {w}) = (0). V or (Lin {v}) /\ (Lin {w}) <> (0). V ) ;

suppose (Lin {v}) /\ (Lin {w}) = (0). V ; :: thesis: rank (W + (Lin {v})) = rank W

then consider w1, w2 being Vector of V such that
D2: ( w1 <> 0. V & w2 <> 0. V & (LIw + (Lin {v})) + (Lin {w}) = (LIw + (Lin {w1})) + (Lin {w2}) & LIw /\ (Lin {w1}) <> (0). V & (LIw + (Lin {w1})) /\ (Lin {w2}) = (0). V & v in (Lin {w1}) + (Lin {w2}) & w in (Lin {w1}) + (Lin {w2}) & w1 in (Lin {v}) + (Lin {w}) & w2 in (Lin {v}) + (Lin {w}) ) by B2, B6, LmSumMod3, C1;
(Omega). (Lin {v}) = Lin {v} ;
then D3: W + (Lin {v}) = ((Lin (I \ {w})) + (Lin {w})) + (Lin {v}) by B6, ZMODUL04:22
.= ((Lin (I \ {w})) + (Lin {w1})) + (Lin {w2}) by D2, ZMODUL01:96 ;
D4: rank (LIw + (Lin {w1})) = n + 1 by B10, B1, D2;
rank (W + (Lin {v})) = (rank ((Lin (I \ {w})) + (Lin {w1}))) + (rank (Lin {w2})) by D3, D2, ThRankDirectSum
.= (n + 1) + 1 by D4, D2, LmRank0a
.= n + 2 ;
hence rank (W + (Lin {v})) = rank W by B2; :: thesis: verum

end;

suppose D1: (Lin {v}) /\ (Lin {w}) <> (0). V ; :: thesis: rank (W + (Lin {v})) = rank W

consider u being Vector of V such that
D2: ( u <> 0. V & (Lin {v}) + (Lin {w}) = Lin {u} ) by B2, B6, D1, LmSumMod2;
(Omega). (Lin {v}) = Lin {v} ;
then D3: W + (Lin {v}) = ((Lin (I \ {w})) + (Lin {w})) + (Lin {v}) by B6, ZMODUL04:22
.= (Lin (I \ {w})) + (Lin {u}) by D2, ZMODUL01:96 ;
(Lin (I \ {w})) /\ (Lin {u}) = (0). V

proof

assume (Lin (I \ {w})) /\ (Lin {u}) <> (0). V ; :: thesis: contradiction
then consider x being Vector of V such that
E2: ( x in (Lin (I \ {w})) /\ (Lin {u}) & x <> 0. V ) by ZMODUL04:24;
x in Lin {u} by E2, ZMODUL01:94;
then consider iux being Element of INT.Ring such that
E3: x = iux * u by ThLin1;
w in Lin {w} by ZMODUL02:65, ZFMISC_1:31;
then w in Lin {u} by D2, ZMODUL01:93;
then consider iuw being Element of INT.Ring such that
E4: w = iuw * u by ThLin1;
E5: iux * w in Lin {w} by ZMODUL01:37, ThLin2;
iux * w = (iux * iuw) * u by VECTSP_1:def 16, E4
.= iuw * x by E3, VECTSP_1:def 16 ;
then iux * w in (Lin (I \ {w})) /\ (Lin {u}) by E2, ZMODUL01:37;
then iux * w in Lin (I \ {w}) by ZMODUL01:94;
then E6: iux * w in (Lin (I \ {w})) /\ (Lin {w}) by E5, ZMODUL01:94;
iux <> 0. INT.Ring by E2, E3, ZMODUL01:1;
hence contradiction by E6, ZMODUL02:66, B6, ZMODUL01:def 7; :: thesis: verum

end;

then rank (LIw + (Lin {u})) = (rank LIw) + (rank (Lin {u})) by ThRankDirectSum
.= (n + 1) + 1 by B10, D2, LmRank0a
.= n + 2 ;
hence rank (W + (Lin {v})) = rank W by B2, D3; :: thesis: verum

end;

end;

end;

end;

end;

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

proof

assume (rank W) - 1 is not Nat ; :: thesis: contradiction
then rank W = 0 ;
then B1: (Omega). W = (0). W by ZMODUL05:1
.= (0). V by ZMODUL01:51 ;
(Omega). (Lin {v}) = Lin {v} ;
then W /\ (Lin {v}) = ((0). V) /\ (Lin {v}) by B1, ZMODUL04:23
.= (0). V by ZMODUL01:107 ;
hence contradiction by A4; :: thesis: verum

end;

then reconsider rk1 = (rank W) - 1 as Nat ;
S₁[rk1] by A3;
hence rank (W + (Lin {v})) = rank W by A4; :: thesis: verum