let x be set ; :: thesis:
let V be RealLinearSpace; :: thesis:
let A be Subset of V; :: thesis:
assume A1: x in A ; :: thesis:
then reconsider v = x as VECTOR of V ;
consider f being Function of the carrier of V,REAL such that
A2: f . v = In (1,REAL) 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

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in Carrier f ; :: thesis:
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:

end;

then reconsider f = f as Linear_Combination of {v} by RLVECT_2:def 6;
A7: Sum f = (f . v) * v by RLVECT_2:32
.= v by A2, 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;
rng f c= INT

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume A8: y in rng f ; :: thesis:
consider x being object such that
A9: ( x in the carrier of V & y = f . x ) by A8, FUNCT_2:11;
reconsider z = x as VECTOR of V by A9;

end;

end;