let r be Real; :: thesis: for f being PartFunc of REAL,REAL
for X being set st 0 < r & f is_strictly_convex_on X holds
r (#) f is_strictly_convex_on X
let f be PartFunc of REAL,REAL; :: thesis: for X being set st 0 < r & f is_strictly_convex_on X holds
r (#) f is_strictly_convex_on X
let X be set ; :: thesis: ( 0 < r & f is_strictly_convex_on X implies r (#) f is_strictly_convex_on X )
assume A1: 0 < r ; :: thesis: ( not f is_strictly_convex_on X or r (#) f is_strictly_convex_on X )
assume A2: f is_strictly_convex_on X ; :: thesis: r (#) f is_strictly_convex_on X
then X c= dom f ;
then A3: X c= dom (r (#) f) by VALUED_1:def 5;
for p being Real st 0 < p & p < 1 holds
for t, s being Real st t in X & s in X & (p * t) + ((1 - p) * s) in X & t <> s holds
(r (#) f) . ((p * t) + ((1 - p) * s)) < (p * ((r (#) f) . t)) + ((1 - p) * ((r (#) f) . s))

proof

let p be Real; :: thesis: ( 0 < p & p < 1 implies for t, s being Real st t in X & s in X & (p * t) + ((1 - p) * s) in X & t <> s holds
(r (#) f) . ((p * t) + ((1 - p) * s)) < (p * ((r (#) f) . t)) + ((1 - p) * ((r (#) f) . s)) )
assume A4: ( 0 < p & p < 1 ) ; :: thesis: for t, s being Real st t in X & s in X & (p * t) + ((1 - p) * s) in X & t <> s holds
(r (#) f) . ((p * t) + ((1 - p) * s)) < (p * ((r (#) f) . t)) + ((1 - p) * ((r (#) f) . s))
for t, s being Real st t in X & s in X & (p * t) + ((1 - p) * s) in X & t <> s holds
(r (#) f) . ((p * t) + ((1 - p) * s)) < (p * ((r (#) f) . t)) + ((1 - p) * ((r (#) f) . s))

proof

let t, s be Real; :: thesis: ( t in X & s in X & (p * t) + ((1 - p) * s) in X & t <> s implies (r (#) f) . ((p * t) + ((1 - p) * s)) < (p * ((r (#) f) . t)) + ((1 - p) * ((r (#) f) . s)) )
assume that
A5: ( t in X & s in X ) and
A6: (p * t) + ((1 - p) * s) in X and
A7: t <> s ; :: thesis: (r (#) f) . ((p * t) + ((1 - p) * s)) < (p * ((r (#) f) . t)) + ((1 - p) * ((r (#) f) . s))
f . ((p * t) + ((1 - p) * s)) < (p * (f . t)) + ((1 - p) * (f . s)) by A2, A4, A5, A6, A7;
then A8: r * (f . ((p * t) + ((1 - p) * s))) < r * ((p * (f . t)) + ((1 - p) * (f . s))) by A1, XREAL_1:68;
( p * ((r (#) f) . t) = p * (r * (f . t)) & (1 - p) * ((r (#) f) . s) = (1 - p) * (r * (f . s)) ) by A3, A5, VALUED_1:def 5;
hence (r (#) f) . ((p * t) + ((1 - p) * s)) < (p * ((r (#) f) . t)) + ((1 - p) * ((r (#) f) . s)) by A3, A6, A8, VALUED_1:def 5; :: thesis: verum

end;

hence for t, s being Real st t in X & s in X & (p * t) + ((1 - p) * s) in X & t <> s holds
(r (#) f) . ((p * t) + ((1 - p) * s)) < (p * ((r (#) f) . t)) + ((1 - p) * ((r (#) f) . s)) ; :: thesis: verum

end;

hence r (#) f is_strictly_convex_on X by A3; :: thesis: verum