let X be RealLinearSpace; :: thesis: 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 )

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

assume A1: for x being VECTOR of X holds f . x <> -infty ; :: thesis: ( 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 )

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: ( ( 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 )

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: verum

( 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 )

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

assume A1: for x being VECTOR of X holds f . x <> -infty ; :: thesis: ( 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 )

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: ( ( 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 )

proof

thus
( ( for n being non zero Element of NAT
assume A2:
f is convex
; :: thesis: 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

let n be non zero Element of NAT ; :: thesis: 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

let p be FinSequence of REAL ; :: thesis: 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

let F be FinSequence of ExtREAL ; :: thesis: 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

let y, z be FinSequence of the carrier of X; :: thesis: ( 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)) ) ) implies f . (Sum z) <= Sum F )

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: f . (Sum z) <= Sum F

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;

end;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

let n be non zero Element of NAT ; :: thesis: 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

let p be FinSequence of REAL ; :: thesis: 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

let F be FinSequence of ExtREAL ; :: thesis: 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

let y, z be FinSequence of the carrier of X; :: thesis: ( 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)) ) ) implies f . (Sum z) <= Sum F )

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: f . (Sum z) <= Sum F

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;

per cases
( for i being Element of NAT st i in Seg n holds

f . (y /. i) <> +infty or ex i being Element of NAT st

( i in Seg n & f . (y /. i) = +infty ) ) ;

end;

f . (y /. i) <> +infty or ex i being Element of NAT st

( i in Seg n & f . (y /. i) = +infty ) ) ;

suppose A9:
for i being Element of NAT st i in Seg n holds

f . (y /. i) <> +infty ; :: thesis: f . (Sum z) <= Sum F

f . (y /. i) <> +infty ; :: thesis: f . (Sum z) <= Sum F

defpred S_{1}[ 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

ex v being Element of V st S_{1}[i,v]

A12: dom g = Seg n and

A13: for i being Nat st i in Seg n holds

S_{1}[i,g /. i]
from RECDEF_1:sch 17(A11);

A14: len g = n by A12, FINSEQ_1:def 3;

defpred S_{2}[ 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_{2}[i,w]

A17: dom F1 = Seg n and

A18: for i being Nat st i in Seg n holds

S_{2}[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_{1}( 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_{1}(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 )

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

G . i = [(z . i),(F1 . i)]

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: verum

end;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

A11:
for i being Nat st i in Seg n holds
let i be Element of NAT ; :: thesis: ( i in Seg n implies f . (y /. i) in REAL )

assume i in Seg n ; :: thesis: f . (y /. i) in REAL

then f . (y /. i) <> +infty by A9;

hence f . (y /. i) in REAL by A1, XXREAL_0:14; :: thesis: verum

end;assume i in Seg n ; :: thesis: f . (y /. i) in REAL

then f . (y /. i) <> +infty by A9;

hence f . (y /. i) in REAL by A1, XXREAL_0:14; :: thesis: verum

ex v being Element of V st S

proof

consider g being FinSequence of the carrier of V such that
let i be Nat; :: thesis: ( i in Seg n implies ex v being Element of V st S_{1}[i,v] )

assume i in Seg n ; :: thesis: ex v being Element of V st S_{1}[i,v]

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: S_{1}[i,v]

thus S_{1}[i,v]
; :: thesis: verum

end;assume i in Seg n ; :: thesis: ex v being Element of V st S

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: S

thus S

A12: dom g = Seg n and

A13: for i being Nat st i in Seg n holds

S

A14: len g = n by A12, FINSEQ_1:def 3;

defpred S

A15: for i being Nat st i in Seg n holds

ex w being Element of RLS_Real st S

proof

consider F1 being FinSequence of the carrier of RLS_Real such that
let i be Nat; :: thesis: ( i in Seg n implies ex w being Element of RLS_Real st S_{2}[i,w] )

assume A16: i in Seg n ; :: thesis: ex w being Element of RLS_Real st S_{2}[i,w]

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: S_{2}[i,w]

thus S_{2}[i,w]
; :: thesis: verum

end;assume A16: i in Seg n ; :: thesis: ex w being Element of RLS_Real st S

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: S

thus S

A17: dom F1 = Seg n and

A18: for i being Nat st i in Seg n holds

S

A19: len F1 = n by A17, FINSEQ_1:def 3;

reconsider M = epigraph f as Subset of V ;

deffunc H

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

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

M is convex
by A2;
let i be Nat; :: thesis: ( i in Seg n implies ( p . i > 0 & G . i = (p . i) * (g /. i) & g /. i in M ) )

assume A24: i in Seg n ; :: thesis: ( p . i > 0 & G . i = (p . i) * (g /. i) & g /. i in M )

hence p . i > 0 by A7; :: thesis: ( G . i = (p . i) * (g /. i) & g /. i in M )

thus G . i = (p . i) * (g /. i) by A21, A22, A24; :: thesis: g /. i in M

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: verum

end;assume A24: i in Seg n ; :: thesis: ( p . i > 0 & G . i = (p . i) * (g /. i) & g /. i in M )

hence p . i > 0 by A7; :: thesis: ( G . i = (p . i) * (g /. i) & g /. i in M )

thus G . i = (p . i) * (g /. i) by A21, A22, A24; :: thesis: g /. i in M

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: verum

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

for i being Nat st i in Seg n holds
let i be Element of NAT ; :: thesis: ( i in Seg n implies F1 . i = F . i )

assume A27: i in Seg n ; :: thesis: F1 . i = F . i

then F1 /. i = F1 . i by A17, PARTFUN1:def 6;

hence F1 . i = F . i by A18, A27; :: thesis: verum

end;assume A27: i in Seg n ; :: thesis: F1 . i = F . i

then F1 /. i = F1 . i by A17, PARTFUN1:def 6;

hence F1 . i = F . i by A18, A27; :: thesis: verum

G . i = [(z . i),(F1 . i)]

proof

then
Sum G = [(Sum z),(Sum F1)]
by A5, A20, A19, Th3;
let i be Nat; :: thesis: ( i in Seg n implies G . i = [(z . i),(F1 . i)] )

assume A28: i in Seg n ; :: thesis: G . i = [(z . i),(F1 . i)]

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: verum

end;assume A28: i in Seg n ; :: thesis: G . i = [(z . i),(F1 . i)]

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: verum

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: verum

suppose
ex i being Element of NAT st

( i in Seg n & f . (y /. i) = +infty ) ; :: thesis: f . (Sum z) <= Sum F

( i in Seg n & f . (y /. i) = +infty ) ; :: thesis: f . (Sum z) <= Sum F

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: verum

end;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: verum

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: verum

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: f is convex

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))

end;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: f is convex

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

hence
f is convex
by A1, Th4; :: thesis: verum
set n = 2;

let x1, x2 be VECTOR of X; :: thesis: for q being Real st 0 < q & q < 1 holds

f . ((q * x1) + ((1 - q) * x2)) <= (q * (f . x1)) + ((1 - q) * (f . x2))

let q be Real; :: thesis: ( 0 < q & q < 1 implies f . ((q * x1) + ((1 - q) * x2)) <= (q * (f . x1)) + ((1 - q) * (f . x2)) )

assume that

A37: 0 < q and

A38: q < 1 ; :: thesis: f . ((q * x1) + ((1 - q) * x2)) <= (q * (f . x1)) + ((1 - q) * (f . x2))

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)) )

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: verum

end;let x1, x2 be VECTOR of X; :: thesis: for q being Real st 0 < q & q < 1 holds

f . ((q * x1) + ((1 - q) * x2)) <= (q * (f . x1)) + ((1 - q) * (f . x2))

let q be Real; :: thesis: ( 0 < q & q < 1 implies f . ((q * x1) + ((1 - q) * x2)) <= (q * (f . x1)) + ((1 - q) * (f . x2)) )

assume that

A37: 0 < q and

A38: q < 1 ; :: thesis: f . ((q * x1) + ((1 - q) * x2)) <= (q * (f . x1)) + ((1 - q) * (f . x2))

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

A45:
len p = 2
by FINSEQ_1:44;
let i be Element of NAT ; :: thesis: ( i in Seg 2 implies ( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (p . i) * (f . (y /. i)) ) )

assume A40: i in Seg 2 ; :: thesis: ( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (p . i) * (f . (y /. i)) )

end;assume A40: i in Seg 2 ; :: thesis: ( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (p . i) * (f . (y /. i)) )

per cases
( i = 1 or i = 2 )
by A40, FINSEQ_1:2, TARSKI:def 2;

end;

suppose A41:
i = 1
; :: thesis: ( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (p . i) * (f . (y /. i)) )

then A42:
y /. i = x1
by FINSEQ_4:17;

p . i = q by A41, FINSEQ_1:44;

hence ( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (p . i) * (f . (y /. i)) ) by A37, A41, A42, FINSEQ_1:44; :: thesis: verum

end;p . i = q by A41, FINSEQ_1:44;

hence ( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (p . i) * (f . (y /. i)) ) by A37, A41, A42, FINSEQ_1:44; :: thesis: verum

suppose A43:
i = 2
; :: thesis: ( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (p . i) * (f . (y /. i)) )

then A44:
y /. i = x2
by FINSEQ_4:17;

p . i = 1 - q by A43, FINSEQ_1:44;

hence ( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (p . i) * (f . (y /. i)) ) by A38, A43, A44, FINSEQ_1:44, XREAL_1:50; :: thesis: verum

end;p . i = 1 - q by A43, FINSEQ_1:44;

hence ( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (p . i) * (f . (y /. i)) ) by A38, A43, A44, FINSEQ_1:44, XREAL_1:50; :: thesis: verum

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: verum