let V be RealLinearSpace; :: 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₁( Element of V) -> Element of REAL = In (0,REAL);
consider f being Function of the carrier of V,REAL such that
A3: f . (0. V) = jj 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,REAL) 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

proof

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

end;

then reconsider f = f as Linear_Combination of V by RLVECT_2:def 3;
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 object ; :: 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 ;
v = 0. V by A4, A7;
hence x in {(0. V)} by A6, TARSKI:def 1; :: thesis: verum

end;

let x be object ; :: 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 RLVECT_2:def 6;
Sum f = (f . (0. V)) * (0. V) by A5, RLVECT_2:35
.= 0. V ;
hence contradiction by A1, A5; :: thesis: verum