let x, y be set ; :: thesis: for V being RealLinearSpace
for I being affinely-independent Subset of V st x in conv I holds
( (x |-- I) . y = 1 iff ( x = y & x in I ) )
let V be RealLinearSpace; :: thesis: for I being affinely-independent Subset of V st x in conv I holds
( (x |-- I) . y = 1 iff ( x = y & x in I ) )
let I be affinely-independent Subset of V; :: thesis: ( x in conv I implies ( (x |-- I) . y = 1 iff ( x = y & x in I ) ) )
assume A1: x in conv I ; :: thesis: ( (x |-- I) . y = 1 iff ( x = y & x in I ) )
then reconsider v = x as Element of V ;

hereby :: thesis: ( x = y & x in I implies (x |-- I) . y = 1 )

assume A2: (x |-- I) . y = 1 ; :: thesis: ( x = y & x in I )
x |-- I is convex by A1, Th71;
then A3: Carrier (x |-- I) = {y} by A2, Th64;
y in {y} by TARSKI:def 1;
then reconsider v = y as Element of V by A3;
conv I c= Affin I by Th65;
hence A4: x = Sum (x |-- I) by A1, Def7
.= ((x |-- I) . v) * v by A3, RLVECT_2:35
.= y by A2, RLVECT_1:def 8 ;
:: thesis: x in I
( Carrier (x |-- I) c= I & v in Carrier (x |-- I) ) by A2, RLVECT_2:def 6;
hence x in I by A4; :: thesis: verum

end;

assume that
A5: x = y and
A6: x in I ; :: thesis: (x |-- I) . y = 1
consider L being Linear_Combination of {v} such that
A7: L . v = jj by RLVECT_4:37;
Carrier L c= {v} by RLVECT_2:def 6;
then A8: sum L = 1 by A7, Th32;
A9: I c= Affin I by Lm7;
{v} c= I by A6, ZFMISC_1:31;
then A10: L is Linear_Combination of I by RLVECT_2:21;
Sum L = 1 * v by A7, RLVECT_2:32
.= v by RLVECT_1:def 8 ;
hence (x |-- I) . y = 1 by A5, A6, A7, A8, A9, A10, Def7; :: thesis: verum