let GF be Field; :: thesis: for V being VectSp of GF
for A being Subset of V st A is linearly-independent holds
not 0. V in A
let V be VectSp of GF; :: thesis: for A being Subset of V st A is linearly-independent holds
not 0. V in A
let A be Subset of V; :: thesis: ( A is linearly-independent implies not 0. V in A )
assume that
A1: A is linearly-independent and
A2: 0. V in A ; :: thesis: contradiction
deffunc H₁( set ) -> Element of the carrier of GF = 0. GF;
consider f being Function of the carrier of V, the carrier of GF such that
A3: f . (0. V) = 1_ GF and
A4: for v being Element of V st v <> 0. V holds
f . v = H₁(v) from FUNCT_2:sch 6();
reconsider f = f as Element of Funcs ( the carrier of V, the carrier of GF) by FUNCT_2:8;
ex T being finite Subset of V st
for v being Vector of V st not v in T holds
f . v = 0. GF

proof

take T = {(0. V)}; :: thesis: for v being Vector of V st not v in T holds
f . v = 0. GF
let v be Vector of V; :: thesis: ( not v in T implies f . v = 0. GF )
assume not v in T ; :: thesis: f . v = 0. GF
then v <> 0. V by TARSKI:def 1;
hence f . v = 0. GF by A4; :: thesis: verum

end;

then reconsider f = f as Linear_Combination of V by VECTSP_6:def 1;
A5: Carrier f = {(0. V)}

proof

thus Carrier f c= {(0. V)} :: according to XBOOLE_0:def 10 :: thesis: {(0. V)} c= Carrier f

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier f or x in {(0. V)} )
assume x in Carrier f ; :: thesis: x in {(0. V)}
then consider v being Vector of V such that
A6: v = x and
A7: f . v <> 0. GF ;
v = 0. V by A4, A7;
hence x in {(0. V)} by A6, TARSKI:def 1; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(0. V)} or x in Carrier f )
assume x in {(0. V)} ; :: thesis: x in Carrier f
then x = 0. V by TARSKI:def 1;
hence x in Carrier f by A3; :: thesis: verum

end;

then Carrier f c= A by A2, ZFMISC_1:31;
then reconsider f = f as Linear_Combination of A by VECTSP_6:def 4;
Sum f = (f . (0. V)) * (0. V) by A5, VECTSP_6:20
.= 0. V by VECTSP_1:15 ;
hence contradiction by A1, A5, Def1; :: thesis: verum