let x, y be set ; 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; 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; ( x in conv I implies ( (x |-- I) . y = 1 iff ( x = y & x in I ) ) )
assume A1:
x in conv I
; ( (x |-- I) . y = 1 iff ( x = y & x in I ) )
then reconsider v = x as Element of V ;
hereby ( x = y & x in I implies (x |-- I) . y = 1 )
end;
assume that
A5:
x = y
and
A6:
x in I
; (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; verum