for X being RealLinearSpace
for f being Function of the carrier of X,ExtREAL st ( for x being VECTOR of X holds f . x <> -infty ) holds
( f is convex iff for n being non zero Element of NAT
for p being FinSequence of REAL
for F being FinSequence of ExtREAL
for y, z being FinSequence of the carrier of X st len p = n & len F = n & len y = n & len z = n & Sum p = 1 & ( for i being Element of NAT st i in Seg n holds
( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (p . i) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum F )