let F be PartFunc of REAL ,REAL ; :: thesis: for X being set
for r being Real holds
( F is_convex_on X iff F - r is_convex_on X )
let X be set ; :: thesis: for r being Real holds
( F is_convex_on X iff F - r is_convex_on X )
let r be Real; :: thesis: ( F is_convex_on X iff F - r is_convex_on X )
A1: dom F = dom (F - r) by VALUED_1:3;
thus ( F is_convex_on X implies F - r is_convex_on X ) :: thesis: ( F - r is_convex_on X implies F is_convex_on X )

proof

assume A2: F is_convex_on X ; :: thesis: F - r is_convex_on X
hence A3: X c= dom (F - r) by A1, Def13; :: according to RFUNCT_3:def 13 :: thesis: for p being Real st 0 <= p & p <= 1 holds
for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X holds
(F - r) . ((p * r) + ((1 - p) * s)) <= (p * ((F - r) . r)) + ((1 - p) * ((F - r) . s))
let p be Real; :: thesis: ( 0 <= p & p <= 1 implies for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X holds
(F - r) . ((p * r) + ((1 - p) * s)) <= (p * ((F - r) . r)) + ((1 - p) * ((F - r) . s)) )
assume A4: ( 0 <= p & p <= 1 ) ; :: thesis: for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X holds
(F - r) . ((p * r) + ((1 - p) * s)) <= (p * ((F - r) . r)) + ((1 - p) * ((F - r) . s))
let x, y be Real; :: thesis: ( x in X & y in X & (p * x) + ((1 - p) * y) in X implies (F - r) . ((p * x) + ((1 - p) * y)) <= (p * ((F - r) . x)) + ((1 - p) * ((F - r) . y)) )
assume A5: ( x in X & y in X & (p * x) + ((1 - p) * y) in X ) ; :: thesis: (F - r) . ((p * x) + ((1 - p) * y)) <= (p * ((F - r) . x)) + ((1 - p) * ((F - r) . y))
then F . ((p * x) + ((1 - p) * y)) <= (p * (F . x)) + ((1 - p) * (F . y)) by A2, A4, Def13;
then A6: (F . ((p * x) + ((1 - p) * y))) - r <= ((p * (F . x)) + ((1 - p) * (F . y))) - r by XREAL_1:11;
((p * (F . x)) + ((1 - p) * (F . y))) - r = (p * ((F . x) - r)) + ((1 - p) * ((F . y) - r))
.= (p * ((F - r) . x)) + ((1 - p) * ((F . y) - r)) by A1, A3, A5, VALUED_1:3
.= (p * ((F - r) . x)) + ((1 - p) * ((F - r) . y)) by A1, A3, A5, VALUED_1:3 ;
hence (F - r) . ((p * x) + ((1 - p) * y)) <= (p * ((F - r) . x)) + ((1 - p) * ((F - r) . y)) by A1, A3, A5, A6, VALUED_1:3; :: thesis: verum

end;

assume A7: F - r is_convex_on X ; :: thesis: F is_convex_on X
hence A8: X c= dom F by A1, Def13; :: according to RFUNCT_3:def 13 :: thesis: for p being Real st 0 <= p & p <= 1 holds
for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X holds
F . ((p * r) + ((1 - p) * s)) <= (p * (F . r)) + ((1 - p) * (F . s))
let p be Real; :: thesis: ( 0 <= p & p <= 1 implies for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X holds
F . ((p * r) + ((1 - p) * s)) <= (p * (F . r)) + ((1 - p) * (F . s)) )
assume A9: ( 0 <= p & p <= 1 ) ; :: thesis: for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X holds
F . ((p * r) + ((1 - p) * s)) <= (p * (F . r)) + ((1 - p) * (F . s))
let x, y be Real; :: thesis: ( x in X & y in X & (p * x) + ((1 - p) * y) in X implies F . ((p * x) + ((1 - p) * y)) <= (p * (F . x)) + ((1 - p) * (F . y)) )
assume A10: ( x in X & y in X & (p * x) + ((1 - p) * y) in X ) ; :: thesis: F . ((p * x) + ((1 - p) * y)) <= (p * (F . x)) + ((1 - p) * (F . y))
then (F - r) . ((p * x) + ((1 - p) * y)) <= (p * ((F - r) . x)) + ((1 - p) * ((F - r) . y)) by A7, A9, Def13;
then A11: (F . ((p * x) + ((1 - p) * y))) - r <= (p * ((F - r) . x)) + ((1 - p) * ((F - r) . y)) by A8, A10, VALUED_1:3;
(p * ((F - r) . x)) + ((1 - p) * ((F - r) . y)) = (p * ((F - r) . x)) + ((1 - p) * ((F . y) - r)) by A8, A10, VALUED_1:3
.= (p * ((F . x) - r)) + (((1 - p) * (F . y)) - ((1 - p) * r)) by A8, A10, VALUED_1:3
.= ((p * (F . x)) + ((1 - p) * (F . y))) - r ;
hence F . ((p * x) + ((1 - p) * y)) <= (p * (F . x)) + ((1 - p) * (F . y)) by A11, XREAL_1:11; :: thesis: verum