reconsider F = f, G = g as continuous Function of T,R^1 by TOPMETR:24, TOPREAL6:83;
consider H being Function of T,R^1 such that
A4: for p being Point of T
for r1, r2 being real number st F . p = r1 & G . p = r2 holds
H . p = r1 - r2 and
A5: H is continuous by JGRAPH_2:31;
reconsider h = H as RealMap of T by TOPMETR:24;
A6: dom h = the carrier of T /\ the carrier of T by FUNCT_2:def 1
.= the carrier of T /\ (dom g) by FUNCT_2:def 1
.= (dom f) /\ (dom g) by FUNCT_2:def 1 ;
( dom (f - g) = (dom f) /\ (dom g) & ( for c being set st c in dom h holds
h . c = (f . c) - (g . c) ) ) by A4, VALUED_1:12;
then h = f - g by A6, VALUED_1:14;
hence f - g is continuous RealMap of T by A5, TOPREAL6:83; :: thesis: verum