for V being RealLinearSpace
for v being VECTOR of V ex L being Convex_Combination of V st
( Sum L = v & ( for A being non empty Subset of V st v in A holds
L is Convex_Combination of A ) )