for X being RealLinearSpace
for M being Subset of X holds
( M is convex iff for n being non zero Nat
for p being FinSequence of REAL
for y, z being FinSequence of the carrier of X st len p = n & len y = n & len z = n & Sum p = 1 & ( for i being Nat st i in Seg n holds
( p . i > 0 & z . i = (p . i) * (y /. i) & y /. i in M ) ) holds
Sum z in M )