for V being RealLinearSpace
for v being VECTOR of V
for A being Subset of V
for L being Linear_Combination of A st L is convex & v <> Sum L & L . v <> 0 holds
ex p being VECTOR of V st
( p in conv (A \ {v}) & Sum L = ((L . v) * v) + ((1 - (L . v)) * p) & ((1 / (L . v)) * (Sum L)) + ((1 - (1 / (L . v))) * p) = v )