let x be set ; :: thesis: for V being RealLinearSpace

for v being VECTOR of V

for I being affinely-independent Subset of V st x in conv I holds

( x |-- I is convex & 0 <= (x |-- I) . v & (x |-- I) . v <= 1 )

let V be RealLinearSpace; :: thesis: for v being VECTOR of V

for I being affinely-independent Subset of V st x in conv I holds

( x |-- I is convex & 0 <= (x |-- I) . v & (x |-- I) . v <= 1 )

let v be VECTOR of V; :: thesis: for I being affinely-independent Subset of V st x in conv I holds

( x |-- I is convex & 0 <= (x |-- I) . v & (x |-- I) . v <= 1 )

let I be affinely-independent Subset of V; :: thesis: ( x in conv I implies ( x |-- I is convex & 0 <= (x |-- I) . v & (x |-- I) . v <= 1 ) )

assume A1: x in conv I ; :: thesis: ( x |-- I is convex & 0 <= (x |-- I) . v & (x |-- I) . v <= 1 )

then reconsider I1 = I as non empty Subset of V ;

conv I1 = { (Sum L) where L is Convex_Combination of I1 : L in ConvexComb V } by CONVEX3:5;

then consider L being Convex_Combination of I1 such that

A2: Sum L = x and

L in ConvexComb V by A1;

( conv I c= Affin I & sum L = 1 ) by Th62, Th65;

then L = x |-- I by A1, A2, Def7;

hence ( x |-- I is convex & 0 <= (x |-- I) . v & (x |-- I) . v <= 1 ) by Th62, Th63; :: thesis: verum

for v being VECTOR of V

for I being affinely-independent Subset of V st x in conv I holds

( x |-- I is convex & 0 <= (x |-- I) . v & (x |-- I) . v <= 1 )

let V be RealLinearSpace; :: thesis: for v being VECTOR of V

for I being affinely-independent Subset of V st x in conv I holds

( x |-- I is convex & 0 <= (x |-- I) . v & (x |-- I) . v <= 1 )

let v be VECTOR of V; :: thesis: for I being affinely-independent Subset of V st x in conv I holds

( x |-- I is convex & 0 <= (x |-- I) . v & (x |-- I) . v <= 1 )

let I be affinely-independent Subset of V; :: thesis: ( x in conv I implies ( x |-- I is convex & 0 <= (x |-- I) . v & (x |-- I) . v <= 1 ) )

assume A1: x in conv I ; :: thesis: ( x |-- I is convex & 0 <= (x |-- I) . v & (x |-- I) . v <= 1 )

then reconsider I1 = I as non empty Subset of V ;

conv I1 = { (Sum L) where L is Convex_Combination of I1 : L in ConvexComb V } by CONVEX3:5;

then consider L being Convex_Combination of I1 such that

A2: Sum L = x and

L in ConvexComb V by A1;

( conv I c= Affin I & sum L = 1 ) by Th62, Th65;

then L = x |-- I by A1, A2, Def7;

hence ( x |-- I is convex & 0 <= (x |-- I) . v & (x |-- I) . v <= 1 ) by Th62, Th63; :: thesis: verum