reconsider F = f as continuous Function of T,R^1 by JORDAN5A:27, TOPMETR:17;
set c = the carrier of T;
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;
hence f . q <> 0 ; :: 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 st F . p = r1 holds
H . p = 1 / r1 and
A2: H is continuous by JGRAPH_2:26;
reconsider h = H as RealMap of T by TOPMETR:17;
A3: now :: thesis: for a being object st a in dom h holds
h . a = (f . a) "
let a be object ; :: 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;
dom h = the carrier of T by FUNCT_2:def 1
.= (dom f) \ (f " {0}) by FUNCT_2:def 1 ;
then h = f ^ by A3, RFUNCT_1:def 2;
hence for b1 being RealMap of T st b1 = f ^ holds
b1 is continuous by A2, JORDAN5A:27; :: thesis: verum