let X be non empty RLSStruct ; :: 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 x1, x2 being VECTOR of X
for p being Real st 0 < p & p < 1 holds
f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) ) :: thesis:

proof

assume f is convex ; :: thesis:
then A2: epigraph f is convex by Def7;
let x1, x2 be VECTOR of X; :: thesis:
let p be Real; :: thesis:
assume A3: ( 0 < p & p < 1 ) ; :: thesis:
set p1 = R_EAL p;
A5: 1 - p > 0 by A3, XREAL_1:52;
set p2 = R_EAL (1 - p);
A7: 0. < R_EAL (1 - p) by A5;

per cases by A1, XXREAL_0:14;

suppose A8: ( f . x1 in REAL & f . x2 in REAL ) ; :: thesis:

then reconsider w1 = f . x1 as Real ;
reconsider w2 = f . x2 as Real by A8;
A9: [x1,w1] in epigraph f

proof

f . x1 <= R_EAL w1 ;
hence [x1,w1] in epigraph f ; :: thesis:

end;

reconsider u1 = [x1,w1] as VECTOR of (Prod_of_RLS X,RLS_Real ) ;
A10: [x2,w2] in epigraph f

proof

f . x2 <= R_EAL w2 ;
hence [x2,w2] in epigraph f ; :: thesis:

end;

reconsider u2 = [x2,w2] as VECTOR of (Prod_of_RLS X,RLS_Real ) ;
A11: (p * u1) + ((1 - p) * u2) in epigraph f by A2, A3, A9, A10, CONVEX1:def 2;
A12: p * u1 = [(p * x1),(p * w1)] by Lm1;
(1 - p) * u2 = [((1 - p) * x2),((1 - p) * w2)] by Lm1;
then [((p * x1) + ((1 - p) * x2)),((p * w1) + ((1 - p) * w2))] in epigraph f by A11, A12, Lm2;
then consider x0 being Element of X, y0 being Element of REAL such that
A13: ( [((p * x1) + ((1 - p) * x2)),((p * w1) + ((1 - p) * w2))] = [x0,y0] & f . x0 <= R_EAL y0 ) ;
A14: ( x0 = (p * x1) + ((1 - p) * x2) & y0 = (p * w1) + ((1 - p) * w2) ) by A13, ZFMISC_1:33;
(p * w1) + ((1 - p) * w2) = ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) by Lm16;
hence f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) by A13, A14; :: thesis:

end;

suppose A15: ( f . x1 = +infty & f . x2 in REAL ) ; :: thesis:

then A16: (R_EAL p) * (f . x1) = +infty by A3, XXREAL_3:def 5;
(R_EAL (1 - p)) * (f . x2) in REAL

proof

reconsider w2 = f . x2 as Real by A15;
(R_EAL (1 - p)) * (f . x2) = (1 - p) * w2 by EXTREAL1:13;
hence (R_EAL (1 - p)) * (f . x2) in REAL ; :: thesis:

end;

then (R_EAL (1 - p)) * (f . x2) <> -infty ;
then ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) = +infty by A16, XXREAL_3:def 2;
hence f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) by XXREAL_0:4; :: thesis:

end;

suppose A17: ( f . x1 in REAL & f . x2 = +infty ) ; :: thesis:

then A18: (R_EAL (1 - p)) * (f . x2) = +infty by A5, XXREAL_3:def 5;
(R_EAL p) * (f . x1) in REAL

proof

reconsider w1 = f . x1 as Real by A17;
(R_EAL p) * (f . x1) = p * w1 by EXTREAL1:13;
hence (R_EAL p) * (f . x1) in REAL ; :: thesis:

end;

then (R_EAL p) * (f . x1) <> -infty ;
then ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) = +infty by A18, XXREAL_3:def 2;
hence f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) by XXREAL_0:4; :: thesis:

end;

suppose ( f . x1 = +infty & f . x2 = +infty ) ; :: thesis:

then ( (R_EAL p) * (f . x1) = +infty & (R_EAL (1 - p)) * (f . x2) = +infty ) by A3, A7, XXREAL_3:def 5;
then ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) = +infty by XXREAL_3:def 2;
hence f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) by XXREAL_0:4; :: thesis:

end;

assume A19: for x1, x2 being VECTOR of X
for p being Real st 0 < p & p < 1 holds
f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) ; :: thesis:
for u1, u2 being VECTOR of (Prod_of_RLS X,RLS_Real )
for p being Real st 0 < p & p < 1 & u1 in epigraph f & u2 in epigraph f holds
(p * u1) + ((1 - p) * u2) in epigraph f

proof

let u1, u2 be VECTOR of (Prod_of_RLS X,RLS_Real ); :: thesis:
let p be Real; :: thesis:
assume A20: ( 0 < p & p < 1 & u1 in epigraph f & u2 in epigraph f ) ; :: thesis:
thus (p * u1) + ((1 - p) * u2) in epigraph f :: thesis:

proof

consider x1 being Element of X, y1 being Element of REAL such that
A21: ( u1 = [x1,y1] & f . x1 <= R_EAL y1 ) by A20;
consider x2 being Element of X, y2 being Element of REAL such that
A22: ( u2 = [x2,y2] & f . x2 <= R_EAL y2 ) by A20;
f . x1 <> +infty by A21, XXREAL_0:9;
then reconsider w1 = f . x1 as Real by A1, XXREAL_0:14;
f . x2 <> +infty by A22, XXREAL_0:9;
then reconsider w2 = f . x2 as Real by A1, XXREAL_0:14;
(p * w1) + ((1 - p) * w2) = ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) by Lm16;
then A23: R_EAL ((p * w1) + ((1 - p) * w2)) = ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) ;
then A24: f . ((p * x1) + ((1 - p) * x2)) <= R_EAL ((p * w1) + ((1 - p) * w2)) by A19, A20;
f . ((p * x1) + ((1 - p) * x2)) <> +infty by A19, A20, A23, XXREAL_0:9;
then reconsider w = f . ((p * x1) + ((1 - p) * x2)) as Real by A1, XXREAL_0:14;
A25: w <= (p * w1) + ((1 - p) * w2) by A24;
w1 <= y1 by A21;
then A26: p * w1 <= p * y1 by A20, XREAL_1:66;
A27: w2 <= y2 by A22;
1 - p > 0 by A20, XREAL_1:52;
then (1 - p) * w2 <= (1 - p) * y2 by A27, XREAL_1:66;
then A28: (p * w1) + ((1 - p) * w2) <= (p * w1) + ((1 - p) * y2) by XREAL_1:8;
(p * w1) + ((1 - p) * y2) <= (p * y1) + ((1 - p) * y2) by A26, XREAL_1:8;
then (p * w1) + ((1 - p) * w2) <= (p * y1) + ((1 - p) * y2) by A28, XXREAL_0:2;
then w <= (p * y1) + ((1 - p) * y2) by A25, XXREAL_0:2;
then f . ((p * x1) + ((1 - p) * x2)) <= R_EAL ((p * y1) + ((1 - p) * y2)) ;
then A29: [((p * x1) + ((1 - p) * x2)),((p * y1) + ((1 - p) * y2))] in { [x,y] where x is Element of X, y is Element of REAL : f . x <= R_EAL y } ;
A30: p * u1 = [(p * x1),(p * y1)] by A21, Lm1;
(1 - p) * u2 = [((1 - p) * x2),((1 - p) * y2)] by A22, Lm1;
hence (p * u1) + ((1 - p) * u2) in epigraph f by A29, A30, Lm2; :: thesis:

end;

then epigraph f is convex by CONVEX1:def 2;
hence f is convex by Def7; :: thesis: