deffunc H₁( set ) -> Element of REAL = zz;
let V be RealUnitarySpace; :: thesis: for A being Subset of V
for x being set st x in A holds
x in Lin A
let A be Subset of V; :: thesis: for x being set st x in A holds
x in Lin A
let x be set ; :: thesis: ( x in A implies x in Lin A )
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₁(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

proof

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;

then reconsider f = f as Linear_Combination of V by RLVECT_2:def 3;
A4: Carrier f c= {v}

proof

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;

then reconsider f = f as Linear_Combination of {v} by RLVECT_2:def 6;
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 Th1; :: thesis: verum