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 H1( 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 = H1(v) from 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 ; :: 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:
then x = 0. V by TARSKI:def 1;
hence x in Carrier f by A3; :: thesis: verum
end;
then Carrier f c= A by ;
then reconsider f = f as Linear_Combination of A by RLVECT_2:def 6;
Sum f = (f . (0. V)) * (0. V) by
.= 0. V ;
hence contradiction by A1, A5; :: thesis: verum