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

proof

let q be Point of T; :: thesis: f . q <> 0
dom f = the carrier of T by FUNCT_2:def 1;
then f . q in rng f by FUNCT_1:def 5;
hence f . 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 being real number st F . p = r1 holds
H . p = 1 / r1 and
A2: H is continuous by JGRAPH_2:36;
reconsider h = H as RealMap of T by TOPMETR:24;
A3: dom h = the carrier of T by FUNCT_2:def 1
.= (dom f) \ (f " {0 }) by FUNCT_2:def 1 ;

now

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

end;

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