let F be PartFunc of REAL , REAL ; :: thesis: for X being set
for r being Real st 0 < r holds
( F is_convex_on X iff r (#) F is_convex_on X )
let X be set ; :: thesis: for r being Real st 0 < r holds
( F is_convex_on X iff r (#) F is_convex_on X )
let r be Real; :: thesis: ( 0 < r implies ( F is_convex_on X iff r (#) F is_convex_on X ) )
assume A1: 0 < r ; :: thesis: ( F is_convex_on X iff r (#) F is_convex_on X )
A2: dom F = dom (r (#) F) by VALUED_1:def 5;
thus ( F is_convex_on X implies r (#) F is_convex_on X ) :: thesis: ( r (#) F is_convex_on X implies F is_convex_on X )

proof

assume A3: F is_convex_on X ; :: thesis: r (#) F is_convex_on X
then A4: X c= dom F by Def13;
thus X c= dom (r (#) F) by A2, A3, 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
(r (#) F) . ((p * r) + ((1 - p) * s)) <= (p * ((r (#) F) . r)) + ((1 - p) * ((r (#) 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
(r (#) F) . ((p * r) + ((1 - p) * s)) <= (p * ((r (#) F) . r)) + ((1 - p) * ((r (#) F) . s)) )
assume A5: ( 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
(r (#) F) . ((p * r) + ((1 - p) * s)) <= (p * ((r (#) F) . r)) + ((1 - p) * ((r (#) F) . s))
let x, y be Real; :: thesis: ( x in X & y in X & (p * x) + ((1 - p) * y) in X implies (r (#) F) . ((p * x) + ((1 - p) * y)) <= (p * ((r (#) F) . x)) + ((1 - p) * ((r (#) F) . y)) )
assume A6: ( x in X & y in X & (p * x) + ((1 - p) * y) in X ) ; :: thesis: (r (#) F) . ((p * x) + ((1 - p) * y)) <= (p * ((r (#) F) . x)) + ((1 - p) * ((r (#) F) . y))
then F . ((p * x) + ((1 - p) * y)) <= (p * (F . x)) + ((1 - p) * (F . y)) by A3, A5, Def13;
then r * (F . ((p * x) + ((1 - p) * y))) <= r * ((p * (F . x)) + ((1 - p) * (F . y))) by A1, XREAL_1:66;
then (r (#) F) . ((p * x) + ((1 - p) * y)) <= (p * (r * (F . x))) + (((1 - p) * r) * (F . y)) by A2, A4, A6, VALUED_1:def 5;
then (r (#) F) . ((p * x) + ((1 - p) * y)) <= (p * ((r (#) F) . x)) + ((1 - p) * (r * (F . y))) by A2, A4, A6, VALUED_1:def 5;
hence (r (#) F) . ((p * x) + ((1 - p) * y)) <= (p * ((r (#) F) . x)) + ((1 - p) * ((r (#) F) . y)) by A2, A4, A6, VALUED_1:def 5; :: thesis: verum

end;

assume A7: r (#) F is_convex_on X ; :: thesis: F is_convex_on X
then A8: X c= dom (r (#) F) by Def13;
hence X c= dom F by VALUED_1:def 5; :: 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 (r (#) F) . ((p * x) + ((1 - p) * y)) <= (p * ((r (#) F) . x)) + ((1 - p) * ((r (#) F) . y)) by A7, A9, Def13;
then r * (F . ((p * x) + ((1 - p) * y))) <= (p * ((r (#) F) . x)) + ((1 - p) * ((r (#) F) . y)) by A8, A10, VALUED_1:def 5;
then r * (F . ((p * x) + ((1 - p) * y))) <= (p * (r * (F . x))) + ((1 - p) * ((r (#) F) . y)) by A8, A10, VALUED_1:def 5;
then r * (F . ((p * x) + ((1 - p) * y))) <= (p * (r * (F . x))) + ((1 - p) * (r * (F . y))) by A8, A10, VALUED_1:def 5;
then (r * (F . ((p * x) + ((1 - p) * y)))) / r <= (r * ((p * (F . x)) + ((1 - p) * (F . y)))) / r by A1, XREAL_1:74;
then F . ((p * x) + ((1 - p) * y)) <= (r * ((p * (F . x)) + ((1 - p) * (F . y)))) / r by A1, XCMPLX_1:90;
hence F . ((p * x) + ((1 - p) * y)) <= (p * (F . x)) + ((1 - p) * (F . y)) by A1, XCMPLX_1:90; :: thesis: verum