let F be Field; :: thesis: for V being VectSp of F
for A being Subset of V st A is linearly-independent holds
for a being Element of V st a nin the carrier of (Lin A) holds
A \/ {a} is linearly-independent
let V be VectSp of F; :: thesis: for A being Subset of V st A is linearly-independent holds
for a being Element of V st a nin the carrier of (Lin A) holds
A \/ {a} is linearly-independent
let A be Subset of V; :: thesis: ( A is linearly-independent implies for a being Element of V st a nin the carrier of (Lin A) holds
A \/ {a} is linearly-independent )
assume Z0: A is linearly-independent ; :: thesis: for a being Element of V st a nin the carrier of (Lin A) holds
A \/ {a} is linearly-independent
let a be Element of V; :: thesis: ( a nin the carrier of (Lin A) implies A \/ {a} is linearly-independent )
set B = A \/ {a};
assume Z1: ( a nin the carrier of (Lin A) & not A \/ {a} is linearly-independent ) ; :: thesis: contradiction
then consider l being Linear_Combination of A \/ {a} such that
A0: ( Sum l = 0. V & Carrier l <> {} ) by VECTSP_7:def 1;
A1: { (Sum s) where s is Linear_Combination of A : verum } = the carrier of (Lin A) by VECTSP_7:def 2;
a in {a} by TARSKI:def 1;
then A2: (l ! {a}) . a = l . a by RANKNULL:25;
A c= the carrier of (Lin A)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in the carrier of (Lin A) )
assume B0: x in A ; :: thesis: x in the carrier of (Lin A)
then reconsider x = x as Element of V ;
x in Lin A by B0, VECTSP_7:13;
hence x in the carrier of (Lin A) by STRUCT_0:def 5; :: thesis: verum

end;

then a nin A by Z1;
then ( (A \/ {a}) \ A = {a} & A c= A \/ {a} ) by XBOOLE_1:7, XBOOLE_1:88, ZFMISC_1:56;
then l = (l ! A) + (l ! {a}) by RANKNULL:27;
then 0. V = (Sum (l ! A)) + (Sum (l ! {a})) by A0, VECTSP_6:77
.= (Sum (l ! A)) + ((l . a) * a) by A2, VECTSP_6:43 ;
then A3: (l . a) * a = - (Sum (l ! A)) by ALGSTR_0:def 13;
A4: (- ((l . a) " )) * (l ! A) is Linear_Combination of A by VECTSP_6:61;

now

assume l . a <> 0. F ; :: thesis: contradiction
then a = ((l . a) " ) * (- (Sum (l ! A))) by A3, VECTSP_1:67
.= - (((l . a) " ) * (Sum (l ! A))) by VECTSP_1:69
.= (- ((l . a) " )) * (Sum (l ! A)) by VECTSP_1:68
.= Sum ((- ((l . a) " )) * (l ! A)) by VECTSP_6:78 ;
hence contradiction by A1, Z1, A4; :: thesis: verum

end;

then A5: ( a nin Carrier l & Carrier l c= A \/ {a} ) by VECTSP_6:20, VECTSP_6:def 7;
Carrier l c= A

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier l or x in A )
thus ( not x in Carrier l or x in A ) by A5, SETWISEO:6; :: thesis: verum

end;

then l is Linear_Combination of A by VECTSP_6:def 7;
hence contradiction by A0, Z0, VECTSP_7:def 1; :: thesis: verum