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 ) )
A1: dom ((1 / r) (#) (r (#) f)) = dom (r (#) f) by VALUED_1:def 5;
assume A2: 0 < r ; :: thesis: ( f is_strictly_convex_on X iff r (#) f is_strictly_convex_on X )
A3: 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 A1, VALUED_1:def 5
.= (1 / r) * (r * (f . x)) by A4, VALUED_1:def 5
.= ((1 / r) * r) * (f . x)
.= 1 * (f . x) by A2, XCMPLX_1:106 ;
hence ((1 / r) (#) (r (#) f)) . x = f . x ; :: thesis: verum
end;
dom (r (#) f) = dom f by VALUED_1:def 5;
then (1 / r) (#) (r (#) f) = f by A1, A3, PARTFUN1:5;
hence ( f is_strictly_convex_on X iff r (#) f is_strictly_convex_on X ) by A2, Lm2, XREAL_1:139; :: thesis: verum