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_{1}( 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_{1}(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

A5: Carrier f = {(0. V)}

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

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

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

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

then reconsider f = f as Linear_Combination of V by RLVECT_2:def 3;
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;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

A5: Carrier f = {(0. V)}

proof

then
Carrier f c= A
by A2, ZFMISC_1:31;
thus
Carrier f c= {(0. V)}
:: according to XBOOLE_0:def 10 :: thesis: {(0. V)} c= 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;proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(0. V)} or x in Carrier f )
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;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

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

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