let x be object ; :: thesis: for V being RealLinearSpace

for A being Subset of V st x in A holds

x in Lin A

let V be RealLinearSpace; :: thesis: for A being Subset of V st x in A holds

x in Lin A

let A be Subset of V; :: thesis: ( x in A implies x in Lin A )

deffunc H_{1}( Element of V) -> Element of REAL = In (0,REAL);

assume A1: x in A ; :: thesis: x in Lin A

then reconsider v = x as VECTOR of V ;

consider f being Function of the carrier of V,REAL such that

A2: f . v = jj and

A3: for u being VECTOR of V st u <> v holds

f . u = H_{1}(u)
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 u being VECTOR of V st not u in T holds

f . u = 0

A4: Carrier f c= {v}

A7: Sum f = 1 * v by A2, RLVECT_2:32

.= v by RLVECT_1:def 8 ;

{v} c= A by A1, ZFMISC_1:31;

then Carrier f c= A by A4;

then reconsider f = f as Linear_Combination of A by RLVECT_2:def 6;

Sum f = v by A7;

hence x in Lin A by Th14; :: thesis: verum

for A being Subset of V st x in A holds

x in Lin A

let V be RealLinearSpace; :: thesis: for A being Subset of V st x in A holds

x in Lin A

let A be Subset of V; :: thesis: ( x in A implies x in Lin A )

deffunc H

assume A1: x in A ; :: thesis: x in Lin A

then reconsider v = x as VECTOR of V ;

consider f being Function of the carrier of V,REAL such that

A2: f . v = jj and

A3: for u being VECTOR of V st u <> v holds

f . u = 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 u being VECTOR of V st not u in T holds

f . u = 0

proof

then reconsider f = f as Linear_Combination of V by RLVECT_2:def 3;
take T = {v}; :: thesis: for u being VECTOR of V st not u in T holds

f . u = 0

let u be VECTOR of V; :: thesis: ( not u in T implies f . u = 0 )

assume not u in T ; :: thesis: f . u = 0

then u <> v by TARSKI:def 1;

hence f . u = 0 by A3; :: thesis: verum

end;f . u = 0

let u be VECTOR of V; :: thesis: ( not u in T implies f . u = 0 )

assume not u in T ; :: thesis: f . u = 0

then u <> v by TARSKI:def 1;

hence f . u = 0 by A3; :: thesis: verum

A4: Carrier f c= {v}

proof

then reconsider f = f as Linear_Combination of {v} by RLVECT_2:def 6;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier f or x in {v} )

assume x in Carrier f ; :: thesis: x in {v}

then consider u being VECTOR of V such that

A5: x = u and

A6: f . u <> 0 ;

u = v by A3, A6;

hence x in {v} by A5, TARSKI:def 1; :: thesis: verum

end;assume x in Carrier f ; :: thesis: x in {v}

then consider u being VECTOR of V such that

A5: x = u and

A6: f . u <> 0 ;

u = v by A3, A6;

hence x in {v} by A5, TARSKI:def 1; :: thesis: verum

A7: Sum f = 1 * v by A2, RLVECT_2:32

.= v by RLVECT_1:def 8 ;

{v} c= A by A1, ZFMISC_1:31;

then Carrier f c= A by A4;

then reconsider f = f as Linear_Combination of A by RLVECT_2:def 6;

Sum f = v by A7;

hence x in Lin A by Th14; :: thesis: verum