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 ;

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

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 that 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;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

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