let r be Real; :: thesis: for f being PartFunc of REAL,REAL
for X being set st f is_strictly_convex_on X holds
f - r is_strictly_convex_on X
let f be PartFunc of REAL,REAL; :: thesis: for X being set st f is_strictly_convex_on X holds
f - r is_strictly_convex_on X
let X be set ; :: thesis: ( f is_strictly_convex_on X implies f - r is_strictly_convex_on X )
assume A1: f is_strictly_convex_on X ; :: thesis: f - r is_strictly_convex_on X
then A2: X c= dom f by Def1;
A3: 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
(f - r) . ((p * t) + ((1 - p) * s)) < (p * ((f - r) . t)) + ((1 - p) * ((f - r) . 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
(f - r) . ((p * t) + ((1 - p) * s)) < (p * ((f - r) . t)) + ((1 - p) * ((f - r) . 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
(f - r) . ((p * t) + ((1 - p) * s)) < (p * ((f - r) . t)) + ((1 - p) * ((f - r) . s))
for t, s being Real st t in X & s in X & (p * t) + ((1 - p) * s) in X & t <> s holds
(f - r) . ((p * t) + ((1 - p) * s)) < (p * ((f - r) . t)) + ((1 - p) * ((f - r) . s))

proof

let t, s be Real; :: thesis: ( t in X & s in X & (p * t) + ((1 - p) * s) in X & t <> s implies (f - r) . ((p * t) + ((1 - p) * s)) < (p * ((f - r) . t)) + ((1 - p) * ((f - r) . s)) )
assume that
A5: ( t in X & s in X ) and
A6: (p * t) + ((1 - p) * s) in X and
A7: t <> s ; :: thesis: (f - r) . ((p * t) + ((1 - p) * s)) < (p * ((f - r) . t)) + ((1 - p) * ((f - r) . s))
f . ((p * t) + ((1 - p) * s)) < (p * (f . t)) + ((1 - p) * (f . s)) by A1, A4, A5, A6, A7, Def1;
then A8: (f . ((p * t) + ((1 - p) * s))) - r < ((p * (f . t)) + ((1 - p) * (f . s))) - r by XREAL_1:9;
( (f - r) . t = (f . t) - r & (f - r) . s = (f . s) - r ) by A2, A5, VALUED_1:3;
hence (f - r) . ((p * t) + ((1 - p) * s)) < (p * ((f - r) . t)) + ((1 - p) * ((f - r) . s)) by A2, A6, A8, VALUED_1:3; :: 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
(f - r) . ((p * t) + ((1 - p) * s)) < (p * ((f - r) . t)) + ((1 - p) * ((f - r) . s)) ; :: thesis: verum

end;

dom f = dom (f - r) by VALUED_1:3;
hence f - r is_strictly_convex_on X by A2, A3, Def1; :: thesis: verum