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)

( ( for r being Point of X holds g . r = ((f1 . r) * p1) + ((f2 . r) * p2) ) & g is continuous ) by A8; :: thesis: verum

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)

proof

hence
ex g being Function of X,(TOP-REAL n) st
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;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

( ( for r being Point of X holds g . r = ((f1 . r) * p1) + ((f2 . r) * p2) ) & g is continuous ) by A8; :: thesis: verum