let X be non empty TopSpace; :: thesis: for n being Element of NAT
for p1, p2 being Point of (TOP-REAL n)
for f1, f2 being Function of X,R^1 st f1 is continuous & f2 is continuous holds
ex g being Function of X,(TOP-REAL n) st
( ( for r being Point of X holds g . r = ((f1 . r) * p1) + ((f2 . r) * p2) ) & g is continuous )
let n be Element of NAT ; :: thesis: for p1, p2 being Point of (TOP-REAL n)
for f1, f2 being Function of X,R^1 st f1 is continuous & f2 is continuous holds
ex g being Function of X,(TOP-REAL n) 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 (TOP-REAL n); :: thesis: for f1, f2 being Function of X,R^1 st f1 is continuous & f2 is continuous holds
ex g being Function of X,(TOP-REAL n) 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,(TOP-REAL n) st
( ( for r being Point of X holds g . r = ((f1 . r) * p1) + ((f2 . r) * p2) ) & g is continuous ) )
assume A1: ( f1 is continuous & f2 is continuous ) ; :: thesis: ex g being Function of X,(TOP-REAL n) st
( ( for r being Point of X holds g . r = ((f1 . r) * p1) + ((f2 . r) * p2) ) & g is continuous )
then consider g1 being Function of X,(TOP-REAL n) such that
A2: ( ( for r being Point of X holds g1 . r = (f1 . r) * p1 ) & g1 is continuous ) by Th17;
consider g2 being Function of X,(TOP-REAL n) such that
A3: ( ( for r being Point of X holds g2 . r = (f2 . r) * p2 ) & g2 is continuous ) by A1, Th17;
consider g being Function of X,(TOP-REAL n) such that
A4: ( ( for r being Point of X holds g . r = (g1 . r) + (g2 . r) ) & g is continuous ) by A2, A3, Th20;
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 A4;
then g . r = (g1 . r) + ((f2 . r) * p2) by A3;
hence g . r = ((f1 . r) * p1) + ((f2 . r) * p2) by A2; :: thesis: verum

end;

hence ex g being Function of X,(TOP-REAL n) st
( ( for r being Point of X holds g . r = ((f1 . r) * p1) + ((f2 . r) * p2) ) & g is continuous ) by A4; :: thesis: verum