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 A1: 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
A2: { (Sum s) where s is Linear_Combination of A : verum } = the carrier of (Lin A) by VECTSP_7:def 2;
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 that
A3: a nin the carrier of (Lin A) and
A4: A \/ {a} is linearly-dependent ; :: thesis: contradiction
consider l being Linear_Combination of A \/ {a} such that
A5: Sum l = 0. V and
A6: Carrier l <> {} by A4, VECTSP_7:def 1;
a in {a} by TARSKI:def 1;
then A7: (l ! {a}) . a = l . a by RANKNULL:25;
A c= the carrier of (Lin A)

proof

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

end;

then a nin A by A3;
then (A \/ {a}) \ A = {a} by XBOOLE_1:88, ZFMISC_1:50;
then l = (l ! A) + (l ! {a}) by RANKNULL:27, XBOOLE_1:7;
then 0. V = (Sum (l ! A)) + (Sum (l ! {a})) by A5, VECTSP_6:44
.= (Sum (l ! A)) + ((l . a) * a) by A7, VECTSP_6:17 ;
then A9: (l . a) * a = - (Sum (l ! A)) by ALGSTR_0:def 13;
A10: (- ((l . a) ")) * (l ! A) is Linear_Combination of A by VECTSP_6:31;

now :: thesis: not l . a <> 0. F

assume l . a <> 0. F ; :: thesis: contradiction
then a = ((l . a) ") * (- (Sum (l ! A))) by A9, VECTSP_1:20
.= - (((l . a) ") * (Sum (l ! A))) by VECTSP_1:22
.= (- ((l . a) ")) * (Sum (l ! A)) by VECTSP_1:21
.= Sum ((- ((l . a) ")) * (l ! A)) by VECTSP_6:45 ;
hence contradiction by A3, A2, A10; :: thesis: verum

end;

then A11: a nin Carrier l by VECTSP_6:2;
A12: Carrier l c= A \/ {a} by VECTSP_6:def 4;
Carrier l c= A by A11, A12, ZFMISC_1:136;
then l is Linear_Combination of A by VECTSP_6:def 4;
hence contradiction by A1, A5, A6, VECTSP_7:def 1; :: thesis: verum