let a, b be Real; :: thesis: for f, g being PartFunc of REAL,REAL
for X being set st f is_strictly_convex_on X & g is_strictly_convex_on X & ( ( a > 0 & b >= 0 ) or ( a >= 0 & b > 0 ) ) holds
(a (#) f) + (b (#) g) is_strictly_convex_on X
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 & ( ( a > 0 & b >= 0 ) or ( a >= 0 & b > 0 ) ) holds
(a (#) f) + (b (#) g) is_strictly_convex_on X
let X be set ; :: thesis: ( f is_strictly_convex_on X & g is_strictly_convex_on X & ( ( a > 0 & b >= 0 ) or ( a >= 0 & b > 0 ) ) implies (a (#) f) + (b (#) g) is_strictly_convex_on X )
assume that
A1: f is_strictly_convex_on X and
A2: g is_strictly_convex_on X and
A3: ( ( a > 0 & b >= 0 ) or ( a >= 0 & b > 0 ) ) ; :: thesis: (a (#) f) + (b (#) g) is_strictly_convex_on X

now :: thesis: (a (#) f) + (b (#) g) is_strictly_convex_on X

per cases ( ( a > 0 & b > 0 ) or ( a > 0 & b = 0 ) or ( a = 0 & b > 0 ) ) by A3;

suppose ( a > 0 & b > 0 ) ; :: thesis: (a (#) f) + (b (#) g) is_strictly_convex_on X

then ( a (#) f is_strictly_convex_on X & b (#) g is_strictly_convex_on X ) by A1, A2, Th12;
hence (a (#) f) + (b (#) g) is_strictly_convex_on X by Th13; :: thesis: verum

end;

suppose A4: ( a > 0 & b = 0 ) ; :: thesis: (a (#) f) + (b (#) g) is_strictly_convex_on X

A5: X c= dom g by A2;
a (#) f is_strictly_convex_on X by A1, A4, Th12;
hence (a (#) f) + (b (#) g) is_strictly_convex_on X by A4, A5, Th14, RFUNCT_3:57; :: thesis: verum

end;

suppose A6: ( a = 0 & b > 0 ) ; :: thesis: (a (#) f) + (b (#) g) is_strictly_convex_on X

A7: X c= dom f by A1;
b (#) g is_strictly_convex_on X by A2, A6, Th12;
hence (a (#) f) + (b (#) g) is_strictly_convex_on X by A6, A7, Th14, RFUNCT_3:57; :: thesis: verum

end;

end;

end;

hence (a (#) f) + (b (#) g) is_strictly_convex_on X ; :: thesis: verum