let r be Real; :: thesis: for f being PartFunc of REAL,REAL
for X being set holds
( f is_strictly_convex_on X iff f - r is_strictly_convex_on X )
let f be PartFunc of REAL,REAL; :: thesis: for X being set holds
( f is_strictly_convex_on X iff f - r is_strictly_convex_on X )
let X be set ; :: thesis: ( f is_strictly_convex_on X iff f - r is_strictly_convex_on X )
A1: dom (f - r) = dom f by VALUED_1:3;
A2: for x being Element of REAL st x in dom (f - r) holds
((f - r) - (- r)) . x = f . x

proof

let x be Element of REAL ; :: thesis: ( x in dom (f - r) implies ((f - r) - (- r)) . x = f . x )
assume A3: x in dom (f - r) ; :: thesis: ((f - r) - (- r)) . x = f . x
then ((f - r) - (- r)) . x = ((f - r) . x) - (- r) by VALUED_1:3
.= ((f - r) . x) + r
.= ((f . x) - r) + r by A1, A3, VALUED_1:3
.= (f . x) - (r - r) ;
hence ((f - r) - (- r)) . x = f . x ; :: thesis: verum

end;

dom ((f - r) - (- r)) = dom (f - r) by VALUED_1:3;
then (f - r) - (- r) = f by A1, A2, PARTFUN1:5;
hence ( f is_strictly_convex_on X iff f - r is_strictly_convex_on X ) by Lm1; :: thesis: verum