let f, g be PartFunc of REAL ,REAL ; :: thesis: for X being set st f is_strictly_convex_on X & g is_strictly_convex_on X holds
f + g is_strictly_convex_on X
let X be set ; :: thesis: ( f is_strictly_convex_on X & g is_strictly_convex_on X implies f + g is_strictly_convex_on X )
assume A1: ( f is_strictly_convex_on X & g is_strictly_convex_on X ) ; :: thesis: f + g 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;
( X c= dom g & ( 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
g . ((p * r) + ((1 - p) * s)) < (p * (g . r)) + ((1 - p) * (g . s)) ) ) by A1, Def1;
then X c= (dom f) /\ (dom g) by A2, XBOOLE_1:19;
then A3: X c= dom (f + g) by VALUED_1:def 1;
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 + g) . ((p * r) + ((1 - p) * s)) < (p * ((f + g) . r)) + ((1 - p) * ((f + g) . s))

proof

let p be Real; :: thesis: ( 0 < p & p < 1 implies for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s holds
(f + g) . ((p * r) + ((1 - p) * s)) < (p * ((f + g) . r)) + ((1 - p) * ((f + g) . s)) )
assume A4: ( 0 < p & p < 1 ) ; :: thesis: for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s holds
(f + g) . ((p * r) + ((1 - p) * s)) < (p * ((f + g) . r)) + ((1 - p) * ((f + g) . s))
for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s holds
(f + g) . ((p * r) + ((1 - p) * s)) < (p * ((f + g) . r)) + ((1 - p) * ((f + g) . s))

proof

let r, s be Real; :: thesis: ( r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s implies (f + g) . ((p * r) + ((1 - p) * s)) < (p * ((f + g) . r)) + ((1 - p) * ((f + g) . s)) )
assume A5: ( r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s ) ; :: thesis: (f + g) . ((p * r) + ((1 - p) * s)) < (p * ((f + g) . r)) + ((1 - p) * ((f + g) . s))
then A6: ( f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) & g . ((p * r) + ((1 - p) * s)) < (p * (g . r)) + ((1 - p) * (g . s)) ) by A1, A4, Def1;
A7: ((p * (f . r)) + ((1 - p) * (f . s))) + ((p * (g . r)) + ((1 - p) * (g . s))) = (p * ((f . r) + (g . r))) + ((1 - p) * ((f . s) + (g . s))) ;
( (f + g) . ((p * r) + ((1 - p) * s)) = (f . ((p * r) + ((1 - p) * s))) + (g . ((p * r) + ((1 - p) * s))) & (f + g) . r = (f . r) + (g . r) & (f + g) . s = (f . s) + (g . s) ) by A3, A5, VALUED_1:def 1;
hence (f + g) . ((p * r) + ((1 - p) * s)) < (p * ((f + g) . r)) + ((1 - p) * ((f + g) . s)) by A6, A7, XREAL_1:10; :: thesis: verum

end;

hence for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s holds
(f + g) . ((p * r) + ((1 - p) * s)) < (p * ((f + g) . r)) + ((1 - p) * ((f + g) . s)) ; :: thesis: verum

end;

hence f + g is_strictly_convex_on X by A3, Def1; :: thesis: verum