let h be Function of T,(TOP-REAL n); :: thesis: ( h = f <++> g implies h is continuous )
assume A1: h = f <++> g ; :: thesis: h is continuous
consider F being Function of T,(TOP-REAL n) such that
A2: for r being Point of T holds F . r = (f . r) + (g . r) and
A3: F is continuous by JGRAPH_6:12;
F = h
proof
A4: dom h = the carrier of T by FUNCT_2:def 1;
let x be Point of T; :: according to FUNCT_2:def 8 :: thesis: F . x = h . x
thus F . x = (f . x) + (g . x) by A2
.= h . x by A1, A4, VALUED_2:def 45 ; :: thesis: verum
end;
hence h is continuous by A3; :: thesis: verum