let X be RealLinearSpace; :: thesis:
let f be Function of the carrier of X,ExtREAL; :: thesis:
assume A1: for x being VECTOR of X holds f . x <> -infty ; :: thesis:
thus ( f is convex implies 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 ) :: thesis:

assume A2: f is convex ; :: thesis:
let n be non zero Element of NAT ; :: thesis:
let p be FinSequence of REAL ; :: thesis:
let F be FinSequence of ExtREAL ; :: thesis:
let y, z be FinSequence of the carrier of X; :: thesis:
assume that
A3: len p = n and
A4: len F = n and
len y = n and
A5: len z = n and
A6: Sum p = 1 and
A7: 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)) ) ; :: thesis:
for i being Element of NAT st i in Seg n holds
( p . i >= 0 & F . i = (p . i) * (f . (y /. i)) ) by A7;
then A8: not -infty in rng F by A1, A4, Lm13;

suppose A9: for i being Element of NAT st i in Seg n holds
f . (y /. i) <> +infty ; :: thesis:

defpred S₁[ set , set ] means $2 = [(y /. $1),(f . (y /. $1))];
reconsider V = Prod_of_RLS (X,RLS_Real) as RealLinearSpace ;
A10: for i being Element of NAT st i in Seg n holds
f . (y /. i) in REAL

proof

let i be Element of NAT ; :: thesis:
assume i in Seg n ; :: thesis:
then f . (y /. i) <> +infty by A9;
hence f . (y /. i) in REAL by A1, XXREAL_0:14; :: thesis:

end;

A11: for i being Nat st i in Seg n holds
ex v being Element of V st S₁[i,v]

proof

let i be Nat; :: thesis:
assume i in Seg n ; :: thesis:
then reconsider w = f . (y /. i) as Element of REAL by A10;
set v = [(y /. i),w];
reconsider v = [(y /. i),w] as Element of V ;
take v ; :: thesis:
thus S₁[i,v] ; :: thesis:

end;

consider g being FinSequence of the carrier of V such that
A12: dom g = Seg n and
A13: for i being Nat st i in Seg n holds
S₁[i,g /. i] from RECDEF_1:sch 17(A11);
A14: len g = n by A12, FINSEQ_1:def 3;
defpred S₂[ set , set ] means $2 = F . $1;
A15: for i being Nat st i in Seg n holds
ex w being Element of RLS_Real st S₂[i,w]

proof

let i be Nat; :: thesis:
assume A16: i in Seg n ; :: thesis:
then reconsider a = f . (y /. i) as Element of REAL by A10;
F . i = (p . i) * (f . (y /. i)) by A7, A16;
then F . i = (p . i) * a by EXTREAL1:1;
then reconsider w = F . i as Element of RLS_Real by XREAL_0:def 1;
take w ; :: thesis:
thus S₂[i,w] ; :: thesis:

end;

consider F1 being FinSequence of the carrier of RLS_Real such that
A17: dom F1 = Seg n and
A18: for i being Nat st i in Seg n holds
S₂[i,F1 /. i] from RECDEF_1:sch 17(A15);
A19: len F1 = n by A17, FINSEQ_1:def 3;
reconsider M = epigraph f as Subset of V ;
deffunc H₁( Nat) -> Element of the carrier of V = (p . $1) * (g /. $1);
consider G being FinSequence of the carrier of V such that
A20: len G = n and
A21: for i being Nat st i in dom G holds
G . i = H₁(i) from FINSEQ_2:sch 1();
A22: dom G = Seg n by A20, FINSEQ_1:def 3;
A23: for i being Nat st i in Seg n holds
( p . i > 0 & G . i = (p . i) * (g /. i) & g /. i in M )

proof

let i be Nat; :: thesis:
assume A24: i in Seg n ; :: thesis:
hence p . i > 0 by A7; :: thesis:
thus G . i = (p . i) * (g /. i) by A21, A22, A24; :: thesis:
reconsider w = f . (y /. i) as Element of REAL by A10, A24;
[(y /. i),w] in { [x,a] where x is Element of X, a is Element of REAL : f . x <= a } ;
hence g /. i in M by A13, A24; :: thesis:

end;

M is convex by A2;
then A25: Sum G in M by A3, A6, A14, A20, A23, Th7;
A26: for i being Element of NAT st i in Seg n holds
F1 . i = F . i

proof

let i be Element of NAT ; :: thesis:
assume A27: i in Seg n ; :: thesis:
then F1 /. i = F1 . i by A17, PARTFUN1:def 6;
hence F1 . i = F . i by A18, A27; :: thesis:

end;

for i being Nat st i in Seg n holds
G . i = [(z . i),(F1 . i)]

proof

let i be Nat; :: thesis:
assume A28: i in Seg n ; :: thesis:
then reconsider a = f . (y /. i) as Element of REAL by A10;
g /. i = [(y /. i),a] by A13, A28;
then (p . i) * (g /. i) = [((p . i) * (y /. i)),((p . i) * a)] by Lm1;
then G . i = [((p . i) * (y /. i)),((p . i) * a)] by A21, A22, A28;
then A29: G . i = [(z . i),((p . i) * a)] by A7, A28;
F . i = (p . i) * (f . (y /. i)) by A7, A28;
then F . i = (p . i) * a by EXTREAL1:1;
hence G . i = [(z . i),(F1 . i)] by A26, A28, A29; :: thesis:

end;

then Sum G = [(Sum z),(Sum F1)] by A5, A20, A19, Th3;
then [(Sum z),(Sum F)] in M by A4, A25, A26, A19, Lm8;
then consider x being Element of X, w being Element of REAL such that
A30: [(Sum z),(Sum F)] = [x,w] and
A31: f . x <= w ;
x = Sum z by A30, XTUPLE_0:1;
hence f . (Sum z) <= Sum F by A30, A31, XTUPLE_0:1; :: thesis:

end;

suppose ex i being Element of NAT st
( i in Seg n & f . (y /. i) = +infty ) ; :: thesis:

then consider i being Element of NAT such that
A32: i in Seg n and
A33: f . (y /. i) = +infty ;
A34: F . i = (p . i) * (f . (y /. i)) by A7, A32;
A35: i in dom F by A4, A32, FINSEQ_1:def 3;
p . i > 0 by A7, A32;
then F . i = +infty by A33, A34, XXREAL_3:def 5;
then Sum F = +infty by A8, A35, Lm6, FUNCT_1:3;
hence f . (Sum z) <= Sum F by XXREAL_0:4; :: thesis:

end;

thus ( ( 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 ) implies f is convex ) :: thesis:

proof

assume A36: 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 ; :: thesis:
for x1, x2 being VECTOR of X
for q being Real st 0 < q & q < 1 holds
f . ((q * x1) + ((1 - q) * x2)) <= (q * (f . x1)) + ((1 - q) * (f . x2))

proof

set n = 2;
let x1, x2 be VECTOR of X; :: thesis:
let q be Real; :: thesis:
assume that
A37: 0 < q and
A38: q < 1 ; :: thesis:
reconsider q1 = q * (f . x1), q2 = (1 - q) * (f . x2) as R_eal by XXREAL_0:def 1;
reconsider F = <*q1,q2*> as FinSequence of ExtREAL ;
reconsider z = <*(q * x1),((1 - q) * x2)*> as FinSequence of the carrier of X ;
reconsider y = <*x1,x2*> as FinSequence of the carrier of X ;
reconsider q = q as Element of REAL by XREAL_0:def 1;
reconsider q1 = 1 - q as Element of REAL by XREAL_0:def 1;
reconsider p = <*q,q1*> as FinSequence of REAL ;
A39: for i being Element of NAT st i in Seg 2 holds
( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (p . i) * (f . (y /. i)) )

proof

let i be Element of NAT ; :: thesis:
assume A40: i in Seg 2 ; :: thesis:

per cases by A40, FINSEQ_1:2, TARSKI:def 2;

suppose A41: i = 1 ; :: thesis:

then A42: y /. i = x1 by FINSEQ_4:17;
thus ( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (p . i) * (f . (y /. i)) ) by A37, A41, A42; :: thesis:

end;

suppose A43: i = 2 ; :: thesis:

then A44: y /. i = x2 by FINSEQ_4:17;
thus ( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (p . i) * (f . (y /. i)) ) by A38, A43, A44, XREAL_1:50; :: thesis:

end;

A45: len p = 2 by FINSEQ_1:44;
A46: Sum p = q + (1 - q) by RVSUM_1:77
.= 1 ;
A47: len z = 2 by FINSEQ_1:44;
A48: Sum z = (q * x1) + ((1 - q) * x2) by RLVECT_1:45;
A49: len y = 2 by FINSEQ_1:44;
A50: len F = 2 by FINSEQ_1:44;
Sum F = (q * (f . x1)) + ((1 - q) * (f . x2)) by EXTREAL1:9;
hence f . ((q * x1) + ((1 - q) * x2)) <= (q * (f . x1)) + ((1 - q) * (f . x2)) by A36, A45, A50, A49, A47, A46, A39, A48; :: thesis:

end;

hence f is convex by A1, Th4; :: thesis:

end;