let n be Nat; :: thesis: for X being non empty TopSpace
for f1, f2, g being Function of X,(TOP-REAL n) st f1 is continuous & f2 is continuous & ( for p being Point of X holds g . p = (f1 . p) + (f2 . p) ) holds
g is continuous
let X be non empty TopSpace; :: thesis: for f1, f2, g being Function of X,(TOP-REAL n) st f1 is continuous & f2 is continuous & ( for p being Point of X holds g . p = (f1 . p) + (f2 . p) ) holds
g is continuous
let f1, f2, g be Function of X,(TOP-REAL n); :: thesis: ( f1 is continuous & f2 is continuous & ( for p being Point of X holds g . p = (f1 . p) + (f2 . p) ) implies g is continuous )
assume that
A1: ( f1 is continuous & f2 is continuous ) and
A2: for p being Point of X holds g . p = (f1 . p) + (f2 . p) ; :: thesis: g is continuous
consider h being Function of X,(TOP-REAL n) such that
A3: for r being Point of X holds h . r = (f1 . r) + (f2 . r) and
A4: h is continuous by A1, JGRAPH_6:12;
for x being Point of X holds g . x = h . x

proof

let x be Point of X; :: thesis: g . x = h . x
thus g . x = (f1 . x) + (f2 . x) by A2
.= h . x by A3 ; :: thesis: verum

end;

hence g is continuous by A4, FUNCT_2:63; :: thesis: verum