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 & ( 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 & r <> s holds
f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) ) ) by Def1;
A3: dom f = dom (f - r) by VALUED_1:3;
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 A5: ( t in X & s in X & (p * t) + ((1 - p) * s) in X & t <> s ) ; :: thesis: (f - r) . ((p * t) + ((1 - p) * s)) < (p * ((f - r) . t)) + ((1 - p) * ((f - r) . s))
then f . ((p * t) + ((1 - p) * s)) < (p * (f . t)) + ((1 - p) * (f . s)) by A1, A4, Def1;
then A6: (f . ((p * t) + ((1 - p) * s))) - r < ((p * (f . t)) + ((1 - p) * (f . s))) - r by XREAL_1:11;
( (f - r) . t = (f . t) - r & (f - r) . s = (f . s) - r & (f - r) . ((p * t) + ((1 - p) * s)) = (f . ((p * t) + ((1 - p) * 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 A6; :: 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;

hence f - r is_strictly_convex_on X by A2, A3, Def1; :: thesis: verum