let X be non empty TopSpace; :: thesis: for n being 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 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 that
A1: f1 is continuous and
A2: 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 )
consider g1 being Function of X,(TOP-REAL n) such that
A3: for r being Point of X holds g1 . r = (f1 . r) * p1 and
A4: g1 is continuous by A1, Th9;
consider g2 being Function of X,(TOP-REAL n) such that
A5: for r being Point of X holds g2 . r = (f2 . r) * p2 and
A6: g2 is continuous by A2, Th9;
consider g being Function of X,(TOP-REAL n) 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) 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 A8; :: thesis: verum