set c = the carrier of T;
reconsider F = f, G = g as continuous Function of T,R^1 by TOPMETR:24, TOPREAL6:83;
for q being Point of T holds g . q <> 0

proof

let q be Point of T; :: thesis: g . q <> 0
dom g = the carrier of T by FUNCT_2:def 1;
then g . q in rng g by FUNCT_1:def 5;
hence g . q <> 0 by RELAT_1:def 9; :: thesis: verum

end;

then consider H being Function of T,R^1 such that
A1: 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
A2: H is continuous by JGRAPH_2:37;
reconsider h = H as RealMap of T by TOPMETR:24;
A3: 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) \ (g " {0 })) by FUNCT_2:def 1 ;

now

let c be set ; :: thesis: ( c in dom h implies h . c = (f . c) * ((g . c) " ) )
assume c in dom h ; :: thesis: h . c = (f . c) * ((g . c) " )
hence h . c = (f . c) / (g . c) by A1
.= (f . c) * ((g . c) " ) by XCMPLX_0:def 9 ;
:: thesis: verum

end;

then h = f / g by A3, RFUNCT_1:def 4;
hence f / g is continuous RealMap of T by A2, TOPREAL6:83; :: thesis: verum