let X be RealLinearSpace; :: thesis:
let f be Function of the carrier of X, ExtREAL ; :: thesis:
assume A1: for x being VECTOR of holds f . x <> -infty ; :: thesis:
thus ( f is convex implies for n being non empty 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 = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum F ) :: thesis:

proof

assume A2: f is convex ; :: thesis:
let n be non empty 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
A5: len y = n and
A6: len z = n and
A7: Sum p = 1 and
A8: for i being Element of NAT st i in Seg n holds
( p . i >= 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ; :: thesis:
consider s being Permutation of dom p, k being Element of NAT such that
A9: for i being Element of NAT st i in dom p holds
( i in Seg k iff p . (s . i) <> 0 ) by Lm17;
A10: dom p = Seg n by A3, FINSEQ_1:def 3;
then reconsider s1 = s as FinSequence of Seg n by FINSEQ_2:28;
A11: dom F = Seg n by A4, FINSEQ_1:def 3;
then A12: F is Function of Seg n, ExtREAL by FINSEQ_2:30;
then reconsider F' = F * s1 as FinSequence of ExtREAL by FINSEQ_2:36;
A13: F' = (F' | k) ^ (F' /^ k) by RFINSEQ:21;
A14: for i being Element of NAT st 1 <= i & i <= n - k holds
( i + k in Seg n & p . (s . (i + k)) = 0 )

proof

let i be Element of NAT ; :: thesis:
assume that
A15: 1 <= i and
A16: i <= n - k ; :: thesis:
i <= i + k by INT_1:19;
then A17: 1 <= i + k by A15, XXREAL_0:2;
0 + k < i + k by A15, XREAL_1:8;
then A18: not i + k in Seg k by FINSEQ_1:3;
A19: i + k <= (n - k) + k by A16, XREAL_1:8;
then i + k in dom p by A10, A17, FINSEQ_1:3;
hence ( i + k in Seg n & p . (s . (i + k)) = 0 ) by A9, A19, A17, A18, FINSEQ_1:3; :: thesis:

end;

A20: dom z = Seg n by A6, FINSEQ_1:def 3;
then A21: z is Function of Seg n,the carrier of X by FINSEQ_2:30;
then reconsider z' = z * s1 as FinSequence of the carrier of X by FINSEQ_2:36;
dom s = Seg n by A10, FUNCT_2:def 1;
then A22: len s1 = n by FINSEQ_1:def 3;
then A23: len z' = n by A21, FINSEQ_2:37;
A24: Sum (z' /^ k) = 0. X

proof

per cases ;

suppose k >= n ; :: thesis:

then z' /^ k = <*> the carrier of X by A23, FINSEQ_5:35;
hence Sum (z' /^ k) = 0. X by RLVECT_1:60; :: thesis:

end;

suppose A25: k < n ; :: thesis:

for w being set st w in rng (z' /^ k) holds
w in {(0. X)}

proof

reconsider k1 = n - k as Element of NAT by A25, INT_1:18;
let w be set ; :: thesis:
assume w in rng (z' /^ k) ; :: thesis:
then consider i being set such that
A26: i in dom (z' /^ k) and
A27: (z' /^ k) . i = w by FUNCT_1:def 5;
reconsider i = i as Element of NAT by A26;
len (z' /^ k) = k1 by A23, A25, RFINSEQ:def 2;
then A28: i in Seg k1 by A26, FINSEQ_1:def 3;
then A29: 1 <= i by FINSEQ_1:3;
A30: i <= n - k by A28, FINSEQ_1:3;
then s . (i + k) in Seg n by A10, A14, A29, FUNCT_2:7;
then z . (s . (i + k)) = (p . (s . (i + k))) * (y /. (s . (i + k))) by A8;
then A31: z . (s . (i + k)) = 0. X by A14, A29, A30, RLVECT_1:23;
i + k in Seg n by A14, A29, A30;
then i + k in dom z' by A23, FINSEQ_1:def 3;
then z' . (i + k) = 0. X by A31, FUNCT_1:22;
then w = 0. X by A23, A25, A26, A27, RFINSEQ:def 2;
hence w in {(0. X)} by TARSKI:def 1; :: thesis:

end;

then rng (z' /^ k) c= {(0. X)} by TARSKI:def 3;
hence Sum (z' /^ k) = 0. X by Lm14; :: thesis:

end;

A32: p is Function of Seg n, REAL by A10, FINSEQ_2:30;
then reconsider p' = p * s1 as FinSequence of REAL by FINSEQ_2:36;
set k' = min k,n;
reconsider k' = min k,n as Element of NAT ;
p' = (p' | k) ^ (p' /^ k) by RFINSEQ:21;
then A33: Sum p' = (Sum (p' | k)) + (Sum (p' /^ k)) by RVSUM_1:105;
A34: len F' = n by A22, A12, FINSEQ_2:37;
A35: Sum (F' /^ k) = 0.

proof

per cases ;

suppose k >= n ; :: thesis:

hence Sum (F' /^ k) = 0. by A34, Th4, FINSEQ_5:35; :: thesis:

end;

suppose A36: k < n ; :: thesis:

for w being set st w in rng (F' /^ k) holds
w in {0. }

proof

reconsider k1 = n - k as Element of NAT by A36, INT_1:18;
let w be set ; :: thesis:
assume w in rng (F' /^ k) ; :: thesis:
then consider i being set such that
A37: i in dom (F' /^ k) and
A38: (F' /^ k) . i = w by FUNCT_1:def 5;
reconsider i = i as Element of NAT by A37;
len (F' /^ k) = k1 by A34, A36, RFINSEQ:def 2;
then A39: i in Seg k1 by A37, FINSEQ_1:def 3;
then A40: 1 <= i by FINSEQ_1:3;
A41: i <= n - k by A39, FINSEQ_1:3;
then A42: p . (s . (i + k)) = 0 by A14, A40;
i + k in Seg n by A14, A40, A41;
then A43: i + k in dom F' by A34, FINSEQ_1:def 3;
s . (i + k) in Seg n by A10, A14, A40, A41, FUNCT_2:7;
then F . (s . (i + k)) = (R_EAL 0 ) * (f . (y /. (s . (i + k)))) by A8, A42;
then F' . (i + k) = 0. by A43, FUNCT_1:22;
then w = 0. by A34, A36, A37, A38, RFINSEQ:def 2;
hence w in {0. } by TARSKI:def 1; :: thesis:

end;

then rng (F' /^ k) c= {0. } by TARSKI:def 3;
hence Sum (F' /^ k) = 0. by Lm12; :: thesis:

end;

A44: F' | k = F' | (Seg k) by FINSEQ_1:def 15;
then A45: len (F' | k) = k' by A34, FINSEQ_2:24;
for i being Element of NAT st i in Seg n holds
( p . i >= 0 & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) by A8;
then A46: not -infty in rng F by A1, A4, Lm16;
then not -infty in rng F' by FUNCT_1:25;
then A47: not -infty in (rng (F' | k)) \/ (rng (F' /^ k)) by A13, FINSEQ_1:44;
then A48: not -infty in rng (F' /^ k) by XBOOLE_0:def 3;
A49: z' | k = z' | (Seg k) by FINSEQ_1:def 15;
then A50: len (z' | k) = k' by A23, FINSEQ_2:24;
A51: len p' = n by A22, A32, FINSEQ_2:37;
A52: Sum (p' /^ k) = 0

proof

per cases ;

suppose k >= n ; :: thesis:

hence Sum (p' /^ k) = 0 by A51, FINSEQ_5:35, RVSUM_1:102; :: thesis:

end;

suppose A53: k < n ; :: thesis:

for w being set st w in rng (p' /^ k) holds
w in {0 }

proof

reconsider k1 = n - k as Element of NAT by A53, INT_1:18;
let w be set ; :: thesis:
assume w in rng (p' /^ k) ; :: thesis:
then consider i being set such that
A54: i in dom (p' /^ k) and
A55: (p' /^ k) . i = w by FUNCT_1:def 5;
reconsider i = i as Element of NAT by A54;
len (p' /^ k) = k1 by A51, A53, RFINSEQ:def 2;
then A56: i in Seg k1 by A54, FINSEQ_1:def 3;
then A57: 1 <= i by FINSEQ_1:3;
A58: i <= n - k by A56, FINSEQ_1:3;
then i + k in Seg n by A14, A57;
then A59: i + k in dom p' by A51, FINSEQ_1:def 3;
p . (s . (i + k)) = 0 by A14, A57, A58;
then p' . (i + k) = 0 by A59, FUNCT_1:22;
then w = 0 by A51, A53, A54, A55, RFINSEQ:def 2;
hence w in {0 } by TARSKI:def 1; :: thesis:

end;

then rng (p' /^ k) c= {0 } by TARSKI:def 3;
hence Sum (p' /^ k) = 0 by Lm13; :: thesis:

end;

A60: p' | k = p' | (Seg k) by FINSEQ_1:def 15;
then A61: len (p' | k) = k' by A51, FINSEQ_2:24;
not -infty in rng (F' | k) by A47, XBOOLE_0:def 3;
then A62: Sum F' = (Sum (F' | k)) + (Sum (F' /^ k)) by A13, A48, Th7;
Sum F' = Sum F by A10, A11, A46, Th8;
then A63: Sum (F' | k) = Sum F by A62, A35, XXREAL_3:4;
z' = (z' | k) ^ (z' /^ k) by RFINSEQ:21;
then A64: Sum z' = (Sum (z' | k)) + (Sum (z' /^ k)) by RLVECT_1:58;
Sum z' = Sum z by A10, A20, RLVECT_2:9;
then A65: Sum (z' | k) = Sum z by A64, A24, RLVECT_1:def 7;
A66: dom y = Seg n by A5, FINSEQ_1:def 3;
then A67: y is Function of Seg n,the carrier of X by FINSEQ_2:30;
then reconsider y' = y * s1 as FinSequence of the carrier of X by FINSEQ_2:36;
A68: y' | k = y' | (Seg k) by FINSEQ_1:def 15;
len y' = n by A22, A67, FINSEQ_2:37;
then A69: len (y' | k) = k' by A68, FINSEQ_2:24;
A70: p',p are_fiberwise_equipotent by RFINSEQ:17;
then p' | k <> {} by A7, A33, A52, RFINSEQ:22, RVSUM_1:102;
then reconsider k' = k' as non empty Element of NAT by A61;
A71: for i being Element of NAT st i in Seg k' holds
( (p' | k) . i > 0 & (z' | k) . i = ((p' | k) . i) * ((y' | k) /. i) & (F' | k) . i = (R_EAL ((p' | k) . i)) * (f . ((y' | k) /. i)) )

proof

let i be Element of NAT ; :: thesis:
assume A72: i in Seg k' ; :: thesis:
then A73: i in dom (p' | k) by A61, FINSEQ_1:def 3;
then A74: (p' | k) /. i = p' /. i by FINSEQ_4:85;
dom (p' | k) = (dom p') /\ (Seg k) by A60, RELAT_1:90;
then A75: i in dom p' by A73, XBOOLE_0:def 4;
then A76: p' . i = p . (s . i) by FUNCT_1:22;
p' /. i = p' . i by A75, PARTFUN1:def 8;
then A77: (p' | k) . i = p . (s . i) by A73, A74, A76, PARTFUN1:def 8;
A78: i in dom (y' | k) by A69, A72, FINSEQ_1:def 3;
then A79: (y' | k) /. i = y' /. i by FINSEQ_4:85;
dom (y' | k) = (dom y') /\ (Seg k) by A68, RELAT_1:90;
then A80: i in dom y' by A78, XBOOLE_0:def 4;
then A81: y' . i = y . (s . i) by FUNCT_1:22;
A82: i in dom (F' | k) by A45, A72, FINSEQ_1:def 3;
then A83: (F' | k) /. i = F' /. i by FINSEQ_4:85;
dom (F' | k) = (dom F') /\ (Seg k) by A44, RELAT_1:90;
then A84: i in dom F' by A82, XBOOLE_0:def 4;
then A85: F' . i = F . (s . i) by FUNCT_1:22;
F' /. i = F' . i by A84, PARTFUN1:def 8;
then A86: (F' | k) . i = F . (s . i) by A82, A83, A85, PARTFUN1:def 8;
A87: i in dom (z' | k) by A50, A72, FINSEQ_1:def 3;
then A88: (z' | k) /. i = z' /. i by FINSEQ_4:85;
dom (z' | k) = (dom z') /\ (Seg k) by A49, RELAT_1:90;
then A89: i in dom z' by A87, XBOOLE_0:def 4;
then A90: z' . i = z . (s . i) by FUNCT_1:22;
z' /. i = z' . i by A89, PARTFUN1:def 8;
then A91: (z' | k) . i = z . (s . i) by A87, A88, A90, PARTFUN1:def 8;
A92: i in Seg n by A51, A75, FINSEQ_1:def 3;
k' <= k by XXREAL_0:17;
then Seg k' c= Seg k by FINSEQ_1:7;
then A93: p . (s . i) <> 0 by A9, A10, A72, A92;
y' /. i = y' . i by A80, PARTFUN1:def 8;
then A94: (y' | k) /. i = y /. (s . i) by A10, A66, A79, A81, A92, FUNCT_2:7, PARTFUN1:def 8;
s . i in Seg n by A10, A92, FUNCT_2:7;
hence ( (p' | k) . i > 0 & (z' | k) . i = ((p' | k) . i) * ((y' | k) /. i) & (F' | k) . i = (R_EAL ((p' | k) . i)) * (f . ((y' | k) /. i)) ) by A8, A77, A94, A91, A86, A93; :: thesis:

end;

Sum (p' | k) = 1 by A7, A33, A52, A70, RFINSEQ:22;
hence f . (Sum z) <= Sum F by A1, A2, A65, A63, A61, A69, A50, A45, A71, Th13; :: thesis:

end;

thus ( ( for n being non empty 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 = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum F ) implies f is convex ) :: thesis:

proof

assume A95: for n being non empty 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 = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum F ; :: thesis:
for n being non empty 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 = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum F

proof

let n be non empty 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
A96: len p = n and
A97: len F = n and
A98: len y = n and
A99: len z = n and
A100: Sum p = 1 and
A101: for i being Element of NAT st i in Seg n holds
( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ; :: thesis:
for i being Element of NAT st i in Seg n holds
( p . i >= 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) by A101;
hence f . (Sum z) <= Sum F by A95, A96, A97, A98, A99, A100; :: thesis:

end;

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

end;