let r be Real; :: thesis: for f being PartFunc of REAL ,REAL
for X being set st 0 < r holds
( f is_strictly_convex_on X iff r (#) f is_strictly_convex_on X )
let f be PartFunc of REAL ,REAL ; :: thesis: for X being set st 0 < r holds
( f is_strictly_convex_on X iff r (#) f is_strictly_convex_on X )
let X be set ; :: thesis: ( 0 < r implies ( f is_strictly_convex_on X iff r (#) f is_strictly_convex_on X ) )
assume A1: 0 < r ; :: thesis: ( f is_strictly_convex_on X iff r (#) f is_strictly_convex_on X )
then A2: 0 < 1 / r by XREAL_1:141;
A3: ( dom ((1 / r) (#) (r (#) f)) = dom (r (#) f) & dom (r (#) f) = dom f ) by VALUED_1:def 5;
for x being Element of REAL st x in dom (r (#) f) holds
((1 / r) (#) (r (#) f)) . x = f . x

proof

let x be Element of REAL ; :: thesis: ( x in dom (r (#) f) implies ((1 / r) (#) (r (#) f)) . x = f . x )
assume A4: x in dom (r (#) f) ; :: thesis: ((1 / r) (#) (r (#) f)) . x = f . x
then ((1 / r) (#) (r (#) f)) . x = (1 / r) * ((r (#) f) . x) by A3, VALUED_1:def 5
.= (1 / r) * (r * (f . x)) by A4, VALUED_1:def 5
.= ((1 / r) * r) * (f . x)
.= 1 * (f . x) by A1, XCMPLX_1:107 ;
hence ((1 / r) (#) (r (#) f)) . x = f . x ; :: thesis: verum

end;

then (1 / r) (#) (r (#) f) = f by A3, PARTFUN1:34;
hence ( f is_strictly_convex_on X iff r (#) f is_strictly_convex_on X ) by A1, A2, Lm2; :: thesis: verum