let X be non empty TopSpace; :: thesis: for n being Nat
for p1, p2 being Point of ()
for f1, f2 being Function of X,R^1 st f1 is continuous & f2 is continuous holds
ex g being Function of X,() st
( ( for r being Point of X holds g . r = ((f1 . r) * p1) + ((f2 . r) * p2) ) & g is continuous )

let n be Nat; :: thesis: for p1, p2 being Point of ()
for f1, f2 being Function of X,R^1 st f1 is continuous & f2 is continuous holds
ex g being Function of X,() st
( ( for r being Point of X holds g . r = ((f1 . r) * p1) + ((f2 . r) * p2) ) & g is continuous )

let p1, p2 be Point of (); :: thesis: for f1, f2 being Function of X,R^1 st f1 is continuous & f2 is continuous holds
ex g being Function of X,() st
( ( for r being Point of X holds g . r = ((f1 . r) * p1) + ((f2 . r) * p2) ) & g is continuous )

let f1, f2 be Function of X,R^1; :: thesis: ( f1 is continuous & f2 is continuous implies ex g being Function of X,() st
( ( for r being Point of X holds g . r = ((f1 . r) * p1) + ((f2 . r) * p2) ) & g is continuous ) )

assume that
A1: f1 is continuous and
A2: f2 is continuous ; :: thesis: ex g being Function of X,() st
( ( for r being Point of X holds g . r = ((f1 . r) * p1) + ((f2 . r) * p2) ) & g is continuous )

consider g1 being Function of X,() such that
A3: for r being Point of X holds g1 . r = (f1 . r) * p1 and
A4: g1 is continuous by ;
consider g2 being Function of X,() such that
A5: for r being Point of X holds g2 . r = (f2 . r) * p2 and
A6: g2 is continuous by ;
consider g being Function of X,() such that
A7: for r being Point of X holds g . r = (g1 . r) + (g2 . r) and
A8: g is continuous by A4, A6, Th12;
for r being Point of X holds g . r = ((f1 . r) * p1) + ((f2 . r) * p2)
proof
let r be Point of X; :: thesis: g . r = ((f1 . r) * p1) + ((f2 . r) * p2)
g . r = (g1 . r) + (g2 . r) by A7;
then g . r = (g1 . r) + ((f2 . r) * p2) by A5;
hence g . r = ((f1 . r) * p1) + ((f2 . r) * p2) by A3; :: thesis: verum
end;
hence ex g being Function of X,() st
( ( for r being Point of X holds g . r = ((f1 . r) * p1) + ((f2 . r) * p2) ) & g is continuous ) by A8; :: thesis: verum