let a, b be Real; :: thesis: for f being PartFunc of REAL,REAL holds
( f is_strictly_convex_on [.a,b.] iff ( [.a,b.] c= dom f & ( for p being Real st 0 < p & p < 1 holds
for r, s being Real st r in [.a,b.] & s in [.a,b.] & r <> s holds
f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) ) ) )
let f be PartFunc of REAL,REAL; :: thesis: ( f is_strictly_convex_on [.a,b.] iff ( [.a,b.] c= dom f & ( for p being Real st 0 < p & p < 1 holds
for r, s being Real st r in [.a,b.] & s in [.a,b.] & r <> s holds
f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) ) ) )
set ab = { r where r is Real : ( a <= r & r <= b ) } ;
A1: [.a,b.] = { r where r is Real : ( a <= r & r <= b ) } by RCOMP_1:def 1;
thus ( f is_strictly_convex_on [.a,b.] implies ( [.a,b.] c= dom f & ( for p being Real st 0 < p & p < 1 holds
for x, y being Real st x in [.a,b.] & y in [.a,b.] & x <> y holds
f . ((p * x) + ((1 - p) * y)) < (p * (f . x)) + ((1 - p) * (f . y)) ) ) ) :: thesis: ( [.a,b.] c= dom f & ( for p being Real st 0 < p & p < 1 holds
for r, s being Real st r in [.a,b.] & s in [.a,b.] & r <> s holds
f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) ) implies f is_strictly_convex_on [.a,b.] )

proof

assume A2: f is_strictly_convex_on [.a,b.] ; :: thesis: ( [.a,b.] c= dom f & ( for p being Real st 0 < p & p < 1 holds
for x, y being Real st x in [.a,b.] & y in [.a,b.] & x <> y holds
f . ((p * x) + ((1 - p) * y)) < (p * (f . x)) + ((1 - p) * (f . y)) ) )
hence [.a,b.] c= dom f ; :: thesis: for p being Real st 0 < p & p < 1 holds
for x, y being Real st x in [.a,b.] & y in [.a,b.] & x <> y holds
f . ((p * x) + ((1 - p) * y)) < (p * (f . x)) + ((1 - p) * (f . y))
let p be Real; :: thesis: ( 0 < p & p < 1 implies for x, y being Real st x in [.a,b.] & y in [.a,b.] & x <> y holds
f . ((p * x) + ((1 - p) * y)) < (p * (f . x)) + ((1 - p) * (f . y)) )
assume that
A3: 0 < p and
A4: p < 1 ; :: thesis: for x, y being Real st x in [.a,b.] & y in [.a,b.] & x <> y holds
f . ((p * x) + ((1 - p) * y)) < (p * (f . x)) + ((1 - p) * (f . y))
A5: 0 <= 1 - p by A4, XREAL_1:48;
A6: (p * b) + ((1 - p) * b) = b ;
A7: (p * a) + ((1 - p) * a) = a ;
let x, y be Real; :: thesis: ( x in [.a,b.] & y in [.a,b.] & x <> y implies f . ((p * x) + ((1 - p) * y)) < (p * (f . x)) + ((1 - p) * (f . y)) )
assume that
A8: x in [.a,b.] and
A9: y in [.a,b.] and
A10: x <> y ; :: thesis: f . ((p * x) + ((1 - p) * y)) < (p * (f . x)) + ((1 - p) * (f . y))
A11: ex r2 being Real st
( r2 = y & a <= r2 & r2 <= b ) by A1, A9;
then A12: (1 - p) * y <= (1 - p) * b by A5, XREAL_1:64;
A13: ex r1 being Real st
( r1 = x & a <= r1 & r1 <= b ) by A1, A8;
then p * x <= p * b by A3, XREAL_1:64;
then A14: (p * x) + ((1 - p) * y) <= b by A12, A6, XREAL_1:7;
A15: (1 - p) * a <= (1 - p) * y by A5, A11, XREAL_1:64;
p * a <= p * x by A3, A13, XREAL_1:64;
then a <= (p * x) + ((1 - p) * y) by A15, A7, XREAL_1:7;
then (p * x) + ((1 - p) * y) in { r where r is Real : ( a <= r & r <= b ) } by A14;
hence f . ((p * x) + ((1 - p) * y)) < (p * (f . x)) + ((1 - p) * (f . y)) by A1, A2, A3, A4, A8, A9, A10; :: thesis: verum

end;

assume that
A16: [.a,b.] c= dom f and
A17: for p being Real st 0 < p & p < 1 holds
for x, y being Real st x in [.a,b.] & y in [.a,b.] & x <> y holds
f . ((p * x) + ((1 - p) * y)) < (p * (f . x)) + ((1 - p) * (f . y)) ; :: thesis: f is_strictly_convex_on [.a,b.]
thus [.a,b.] c= dom f by A16; :: according to RFUNCT_4:def 1 :: thesis: for p being Real st 0 < p & p < 1 holds
for r, s being Real st r in [.a,b.] & s in [.a,b.] & (p * r) + ((1 - p) * s) in [.a,b.] & r <> s holds
f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s))
let p be Real; :: thesis: ( 0 < p & p < 1 implies for r, s being Real st r in [.a,b.] & s in [.a,b.] & (p * r) + ((1 - p) * s) in [.a,b.] & r <> s holds
f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) )
assume A18: ( 0 < p & p < 1 ) ; :: thesis: for r, s being Real st r in [.a,b.] & s in [.a,b.] & (p * r) + ((1 - p) * s) in [.a,b.] & r <> s holds
f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s))
let x, y be Real; :: thesis: ( x in [.a,b.] & y in [.a,b.] & (p * x) + ((1 - p) * y) in [.a,b.] & x <> y implies f . ((p * x) + ((1 - p) * y)) < (p * (f . x)) + ((1 - p) * (f . y)) )
assume that
A19: ( x in [.a,b.] & y in [.a,b.] ) and
(p * x) + ((1 - p) * y) in [.a,b.] ; :: thesis: ( not x <> y or f . ((p * x) + ((1 - p) * y)) < (p * (f . x)) + ((1 - p) * (f . y)) )
thus ( not x <> y or f . ((p * x) + ((1 - p) * y)) < (p * (f . x)) + ((1 - p) * (f . y)) ) by A17, A18, A19; :: thesis: verum