let f be PartFunc of REAL,REAL; :: thesis:
assume A1: f is_convex_on REAL ; :: thesis:
defpred S₁[ Nat] means for P, E, F being Element of $1 -tuples_on REAL st Sum P = 1 & ( for i being Element of NAT st i in dom P holds
( P . i >= 0 & F . i = f . (E . i) ) ) holds
f . (Sum (mlt (P,E))) <= Sum (mlt (P,F));
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis:
assume A3: S₁[k] ; :: thesis:
let P, E, F be Element of (k + 1) -tuples_on REAL; :: thesis:
assume that
A4: Sum P = 1 and
A5: for i being Element of NAT st i in dom P holds
( P . i >= 0 & F . i = f . (E . i) ) ; :: thesis:
consider E1 being Element of k -tuples_on REAL, e1 being Element of REAL such that
A6: E = E1 ^ <*e1*> by FINSEQ_2:117;
consider F1 being Element of k -tuples_on REAL, f1 being Element of REAL such that
A7: F = F1 ^ <*f1*> by FINSEQ_2:117;
(len F1) + 1 = k + 1 by CARD_1:def 7
.= len P by CARD_1:def 7 ;
then (len F1) + 1 in Seg (len P) by FINSEQ_1:4;
then A8: (len F1) + 1 in dom P by FINSEQ_1:def 3;
A9: f1 = F . ((len F1) + 1) by A7, FINSEQ_1:42
.= f . (E . ((len F1) + 1)) by A5, A8
.= f . (E . (k + 1)) by CARD_1:def 7
.= f . (E . ((len E1) + 1)) by CARD_1:def 7
.= f . e1 by A6, FINSEQ_1:42 ;
consider P1 being Element of k -tuples_on REAL, p1 being Element of REAL such that
A10: P = P1 ^ <*p1*> by FINSEQ_2:117;
reconsider SP = (Sum P1) " as Element of REAL by XREAL_0:def 1;
mlt (P,F) = (mlt (P1,F1)) ^ <*(p1 * f1)*> by A10, A7, Th2;
then A11: Sum (mlt (P,F)) = (1 * (Sum (mlt (P1,F1)))) + (p1 * f1) by RVSUM_1:74;
mlt (P,E) = (mlt (P1,E1)) ^ <*(p1 * e1)*> by A10, A6, Th2;
then A12: Sum (mlt (P,E)) = (1 * (Sum (mlt (P1,E1)))) + (p1 * e1) by RVSUM_1:74;
A13: for i being Nat st i in dom P1 holds
P1 . i >= 0

proof

let i be Nat; :: thesis:
assume A14: i in dom P1 ; :: thesis:
A15: i in Seg (len P1) by A14, FINSEQ_1:def 3;
then A16: 1 <= i by FINSEQ_1:1;
i <= len P1 by A15, FINSEQ_1:1;
then A17: i <= k by CARD_1:def 7;
k <= k + 1 by NAT_1:11;
then i <= k + 1 by A17, XXREAL_0:2;
then i in Seg (k + 1) by A16, FINSEQ_1:1;
then i in Seg (len P) by CARD_1:def 7;
then A18: i in dom P by FINSEQ_1:def 3;
P1 . i = P . i by A10, A14, FINSEQ_1:def 7;
hence P1 . i >= 0 by A5, A18; :: thesis:

end;

then A19: for i being Element of NAT st i in dom P1 holds
P1 . i >= 0 ;

now :: thesis:

per cases ;

suppose A20: Sum P1 = 0 ; :: thesis:

then for i being Element of NAT st i in dom P1 holds
P1 . i = 0 by A19, Th3;
then A21: P1 = k |-> 0 by Th4;
then mlt (P1,E1) = k |-> 0 by Th5;
then A22: Sum (mlt (P1,E1)) = k * 0 by RVSUM_1:80;
mlt (P1,F1) = k |-> 0 by A21, Th5;
then A23: Sum (mlt (P1,F1)) = k * 0 by RVSUM_1:80;
Sum P = 0 + p1 by A10, A20, RVSUM_1:74;
hence f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) by A4, A12, A11, A9, A22, A23; :: thesis:

end;

suppose A24: Sum P1 <> 0 ; :: thesis:

A25: 0 <= Sum P1 by A13, RVSUM_1:84;
A26: for i being Element of NAT st i in dom (((Sum P1) ") * P1) holds
( (((Sum P1) ") * P1) . i >= 0 & F1 . i = f . (E1 . i) )

proof

let i be Element of NAT ; :: thesis:
assume i in dom (((Sum P1) ") * P1) ; :: thesis:
then A27: i in Seg (len (((Sum P1) ") * P1)) by FINSEQ_1:def 3;
then A28: i in Seg k by CARD_1:def 7;
then A29: i in Seg (len P1) by CARD_1:def 7;
then i <= len P1 by FINSEQ_1:1;
then A30: i <= k by CARD_1:def 7;
A31: 1 <= i by A27, FINSEQ_1:1;
k <= k + 1 by NAT_1:11;
then i <= k + 1 by A30, XXREAL_0:2;
then i in Seg (k + 1) by A31, FINSEQ_1:1;
then i in Seg (len P) by CARD_1:def 7;
then A32: i in dom P by FINSEQ_1:def 3;
i in dom P1 by A29, FINSEQ_1:def 3;
then ( (((Sum P1) ") * P1) . i = ((Sum P1) ") * (P1 . i) & P1 . i >= 0 ) by A13, RVSUM_1:45;
hence (((Sum P1) ") * P1) . i >= 0 by A25; :: thesis:
i in Seg (len E1) by A28, CARD_1:def 7;
then i in dom E1 by FINSEQ_1:def 3;
then A33: E . i = E1 . i by A6, FINSEQ_1:def 7;
i in Seg (len F1) by A28, CARD_1:def 7;
then i in dom F1 by FINSEQ_1:def 3;
then F . i = F1 . i by A7, FINSEQ_1:def 7;
hence F1 . i = f . (E1 . i) by A5, A32, A33; :: thesis:

end;

A34: Sum (mlt (P,E)) = (((Sum P1) * ((Sum P1) ")) * (Sum (mlt (P1,E1)))) + (p1 * e1) by A12, A24, XCMPLX_0:def 7
.= ((Sum P1) * (((Sum P1) ") * (Sum (mlt (P1,E1))))) + (p1 * e1)
.= ((Sum P1) * (Sum (SP * (mlt (P1,E1))))) + (p1 * e1) by RVSUM_1:87
.= ((Sum P1) * (Sum (mlt ((SP * P1),E1)))) + (p1 * e1) by FINSEQOP:26 ;
A35: ((Sum P1) ") * (Sum (mlt (P1,F1))) = Sum (SP * (mlt (P1,F1))) by RVSUM_1:87
.= Sum (mlt ((SP * P1),F1)) by FINSEQOP:26 ;
(len P1) + 1 = len P by A10, FINSEQ_2:16;
then (len P1) + 1 in Seg (len P) by FINSEQ_1:4;
then A36: (len P1) + 1 in dom P by FINSEQ_1:def 3;
(Sum P1) + p1 = 1 by A4, A10, RVSUM_1:74;
then A37: p1 = 1 - (Sum P1) ;
Sum (((Sum P1) ") * P1) = ((Sum P1) ") * (Sum P1) by RVSUM_1:87
.= 1 by A24, XCMPLX_0:def 7 ;
then (Sum P1) * (f . (Sum (mlt ((((Sum P1) ") * P1),E1)))) <= (Sum P1) * (((Sum P1) ") * (Sum (mlt (P1,F1)))) by A3, A25, A35, A26, XREAL_1:64;
then A38: ((Sum P1) * (f . (Sum (mlt ((((Sum P1) ") * P1),E1))))) + (p1 * (f . e1)) <= ((Sum P1) * (((Sum P1) ") * (Sum (mlt (P1,F1))))) + (p1 * (f . e1)) by XREAL_1:6;
A39: Sum (mlt ((SP * P1),E1)) in REAL by XREAL_0:def 1;
A40: ((Sum P1) * (Sum (mlt ((SP * P1),E1)))) + (p1 * e1) in REAL by XREAL_0:def 1;
P . ((len P1) + 1) = p1 by A10, FINSEQ_1:42;
then Sum P1 <= 1 by A5, A37, A36, XREAL_1:49;
then f . (Sum (mlt (P,E))) <= ((Sum P1) * (f . (Sum (mlt ((((Sum P1) ") * P1),E1))))) + (p1 * (f . e1)) by A1, A34, A37, A25, RFUNCT_3:def 12, A39, A40;
then f . (Sum (mlt (P,E))) <= (((Sum P1) * ((Sum P1) ")) * (Sum (mlt (P1,F1)))) + (p1 * (f . e1)) by A38, XXREAL_0:2;
hence f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) by A11, A9, A24, XCMPLX_0:def 7; :: thesis:

end;

hence f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) ; :: thesis:

end;

A41: S₁[ 0 ] by RVSUM_1:79;
for k being Nat holds S₁[k] from NAT_1:sch 2(A41, A2);
hence for n being Element of NAT
for P, E, F being Element of n -tuples_on REAL st Sum P = 1 & ( for i being Element of NAT st i in dom P holds
( P . i >= 0 & F . i = f . (E . i) ) ) holds
f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) ; :: thesis: