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

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

hence
h is continuous
by A3; :: thesis: verum
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;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