let a, b be Real; :: thesis:
let f, g be PartFunc of REAL,REAL; :: thesis:
let X be set ; :: thesis:
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:

now :: thesis:

per cases by A3;

suppose ( a > 0 & b > 0 ) ; :: thesis:

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:

end;

suppose A4: ( a > 0 & b = 0 ) ; :: thesis:

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:

end;

suppose A6: ( a = 0 & b > 0 ) ; :: thesis:

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:

end;

end;

end;

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