let K be Field; :: thesis: for V1 being VectSp of K
for U being finite Subset of V1 st U is linearly-independent holds
for u being Vector of V1 st u in U holds
for L being Linear_Combination of U \ {u} holds
( card U = card ((U \ {u}) \/ {(u + (Sum L))}) & (U \ {u}) \/ {(u + (Sum L))} is linearly-independent )
let V1 be VectSp of K; :: thesis: for U being finite Subset of V1 st U is linearly-independent holds
for u being Vector of V1 st u in U holds
for L being Linear_Combination of U \ {u} holds
( card U = card ((U \ {u}) \/ {(u + (Sum L))}) & (U \ {u}) \/ {(u + (Sum L))} is linearly-independent )
set V = V1;
let U be finite Subset of V1; :: thesis: ( U is linearly-independent implies for u being Vector of V1 st u in U holds
for L being Linear_Combination of U \ {u} holds
( card U = card ((U \ {u}) \/ {(u + (Sum L))}) & (U \ {u}) \/ {(u + (Sum L))} is linearly-independent ) )
assume A1: U is linearly-independent ; :: thesis: for u being Vector of V1 st u in U holds
for L being Linear_Combination of U \ {u} holds
( card U = card ((U \ {u}) \/ {(u + (Sum L))}) & (U \ {u}) \/ {(u + (Sum L))} is linearly-independent )
let u be Vector of V1; :: thesis: ( u in U implies for L being Linear_Combination of U \ {u} holds
( card U = card ((U \ {u}) \/ {(u + (Sum L))}) & (U \ {u}) \/ {(u + (Sum L))} is linearly-independent ) )
assume A2: u in U ; :: thesis: for L being Linear_Combination of U \ {u} holds
( card U = card ((U \ {u}) \/ {(u + (Sum L))}) & (U \ {u}) \/ {(u + (Sum L))} is linearly-independent )
defpred S₁[ Nat] means for L being Linear_Combination of U \ {u} st card (Carrier L) = $1 holds
( card U = card ((U \ {u}) \/ {(u + (Sum L))}) & (U \ {u}) \/ {(u + (Sum L))} is linearly-independent );
A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

card U <> 0 by A2;
then reconsider C = (card U) - 1 as Element of NAT by NAT_1:20;
let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: S₁[n] ; :: thesis: S₁[n + 1]
set n1 = n + 1;
let L be Linear_Combination of U \ {u}; :: thesis: ( card (Carrier L) = n + 1 implies ( card U = card ((U \ {u}) \/ {(u + (Sum L))}) & (U \ {u}) \/ {(u + (Sum L))} is linearly-independent ) )
assume A5: card (Carrier L) = n + 1 ; :: thesis: ( card U = card ((U \ {u}) \/ {(u + (Sum L))}) & (U \ {u}) \/ {(u + (Sum L))} is linearly-independent )
consider x being object such that
A6: x in Carrier L by A5, CARD_1:27, XBOOLE_0:def 1;
A7: Carrier L c= U \ {u} by VECTSP_6:def 4;
then x in U by A6, XBOOLE_0:def 5;
then A8: x <> 0. V1 by A1, VECTSP_7:2;
reconsider x = x as Vector of V1 by A6;
x in {x} by TARSKI:def 1;
then x in Lin {x} by VECTSP_7:8;
then consider X being Linear_Combination of {x} such that
A9: x = Sum X by VECTSP_7:7;
set Lx = L . x;
set LxX = (L . x) * X;
( Carrier ((L . x) * X) c= Carrier X & Carrier X c= {x} ) by VECTSP_6:28, VECTSP_6:def 4;
then A10: Carrier ((L . x) * X) c= {x} ;
then ( Carrier (L - ((L . x) * X)) c= (Carrier L) \/ (Carrier ((L . x) * X)) & (Carrier L) \/ (Carrier ((L . x) * X)) c= (Carrier L) \/ {x} ) by VECTSP_6:41, XBOOLE_1:9;
then Carrier (L - ((L . x) * X)) c= (Carrier L) \/ {x} ;
then A11: Carrier (L - ((L . x) * X)) c= Carrier L by A6, ZFMISC_1:40;
then Carrier (L - ((L . x) * X)) c= U \ {u} by A7;
then reconsider LLxX = L - ((L . x) * X) as Linear_Combination of U \ {u} by VECTSP_6:def 4;
A12: x in (U \ {u}) \/ {(u + (Sum LLxX))} by A6, A7, XBOOLE_0:def 3;
A13: (Carrier L) \ {x} c= Carrier (L - ((L . x) * X))

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (Carrier L) \ {x} or y in Carrier (L - ((L . x) * X)) )
assume A14: y in (Carrier L) \ {x} ; :: thesis: y in Carrier (L - ((L . x) * X))
y in Carrier L by A14, XBOOLE_0:def 5;
then consider Y being Vector of V1 such that
A15: y = Y and
A16: L . Y <> 0. K ;
not Y in Carrier ((L . x) * X) by A10, A14, A15, XBOOLE_0:def 5;
then ((L . x) * X) . Y = 0. K ;
then (L - ((L . x) * X)) . Y = (L . Y) - (0. K) by VECTSP_6:40
.= L . Y by RLVECT_1:13 ;
hence y in Carrier (L - ((L . x) * X)) by A15, A16; :: thesis: verum

end;

(X . x) * x = x by A9, VECTSP_6:17
.= (1_ K) * x ;
then A17: X . x = 1_ K by A8, VECTSP10:4;
(L - ((L . x) * X)) . x = (L . x) - (((L . x) * X) . x) by VECTSP_6:40
.= (L . x) - ((L . x) * (1_ K)) by A17, VECTSP_6:def 9
.= (L . x) - (L . x)
.= 0. K by RLVECT_1:5 ;
then not x in Carrier (L - ((L . x) * X)) by VECTSP_6:2;
then Carrier (L - ((L . x) * X)) c= (Carrier L) \ {x} by A11, ZFMISC_1:34;
then A18: Carrier (L - ((L . x) * X)) = (Carrier L) \ {x} by A13;
{x} c= Carrier L by A6, ZFMISC_1:31;
then card (Carrier (L - ((L . x) * X))) = (n + 1) - (card {x}) by A5, A18, CARD_2:44
.= (n + 1) - 1 by CARD_1:30
.= n ;
then A19: (U \ {u}) \/ {(u + (Sum LLxX))} is linearly-independent by A4;
u + (Sum LLxX) in {(u + (Sum LLxX))} by TARSKI:def 1;
then A20: u + (Sum LLxX) in (U \ {u}) \/ {(u + (Sum LLxX))} by XBOOLE_0:def 3;
A21: not u + (Sum L) in U \ {u}

proof

assume u + (Sum L) in U \ {u} ; :: thesis: contradiction
then A22: u + (Sum L) in Lin (U \ {u}) by VECTSP_7:8;
A23: (u + (Sum L)) - (Sum L) = u + ((Sum L) - (Sum L)) by RLVECT_1:def 3
.= u + (0. V1) by RLVECT_1:5
.= u by RLVECT_1:def 4 ;
Sum L in Lin (U \ {u}) by VECTSP_7:7;
hence contradiction by A1, A2, A22, A23, VECTSP_4:23, VECTSP_9:14; :: thesis: verum

end;

card U = C + 1 ;
then card (U \ {u}) = C by A2, STIRL2_1:55;
then A24: card ((U \ {u}) \/ {(u + (Sum L))}) = C + 1 by A21, CARD_2:41;
Sum L = (0. V1) + (Sum L) by RLVECT_1:def 4
.= ((Sum ((L . x) * X)) + (- (Sum ((L . x) * X)))) + (Sum L) by RLVECT_1:5
.= (Sum ((L . x) * X)) + ((Sum L) - (Sum ((L . x) * X))) by RLVECT_1:def 3
.= (Sum ((L . x) * X)) + (Sum LLxX) by VECTSP_6:47
.= ((L . x) * x) + (Sum LLxX) by A9, VECTSP_6:45 ;
then A25: (u + (Sum LLxX)) + ((L . x) * x) = u + (Sum L) by RLVECT_1:def 3;
A26: not u + (Sum LLxX) in U \ {u}

proof

assume u + (Sum LLxX) in U \ {u} ; :: thesis: contradiction
then A27: u + (Sum LLxX) in Lin (U \ {u}) by VECTSP_7:8;
A28: (u + (Sum LLxX)) - (Sum LLxX) = u + ((Sum LLxX) - (Sum LLxX)) by RLVECT_1:def 3
.= u + (0. V1) by RLVECT_1:5
.= u by RLVECT_1:def 4 ;
Sum LLxX in Lin (U \ {u}) by VECTSP_7:7;
hence contradiction by A1, A2, A27, A28, VECTSP_4:23, VECTSP_9:14; :: thesis: verum

end;

then A29: ((U \ {u}) \/ {(u + (Sum LLxX))}) \ {(u + (Sum LLxX))} = U \ {u} by ZFMISC_1:117;
u + (Sum LLxX) <> x by A6, A7, A26;
hence ( card U = card ((U \ {u}) \/ {(u + (Sum L))}) & (U \ {u}) \/ {(u + (Sum L))} is linearly-independent ) by A19, A25, A29, A20, A12, A24, MATRIX13:115; :: thesis: verum

end;

let L be Linear_Combination of U \ {u}; :: thesis: ( card U = card ((U \ {u}) \/ {(u + (Sum L))}) & (U \ {u}) \/ {(u + (Sum L))} is linearly-independent )
A30: S₁[ 0 ]

proof

let L be Linear_Combination of U \ {u}; :: thesis: ( card (Carrier L) = 0 implies ( card U = card ((U \ {u}) \/ {(u + (Sum L))}) & (U \ {u}) \/ {(u + (Sum L))} is linearly-independent ) )
assume card (Carrier L) = 0 ; :: thesis: ( card U = card ((U \ {u}) \/ {(u + (Sum L))}) & (U \ {u}) \/ {(u + (Sum L))} is linearly-independent )
then Carrier L = {} ;
then u + (Sum L) = u + (0. V1) by VECTSP_6:19
.= u by RLVECT_1:def 4 ;
hence ( card U = card ((U \ {u}) \/ {(u + (Sum L))}) & (U \ {u}) \/ {(u + (Sum L))} is linearly-independent ) by A1, A2, ZFMISC_1:116; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A30, A3);
then S₁[ card (Carrier L)] ;
hence ( card U = card ((U \ {u}) \/ {(u + (Sum L))}) & (U \ {u}) \/ {(u + (Sum L))} is linearly-independent ) ; :: thesis: verum