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

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;

.= (dom f) \ (f " {0}) by FUNCT_2:def 1 ;

then h = f ^ by A3, RFUNCT_1:def 2;

hence for b_{1} being RealMap of T st b_{1} = f ^ holds

b_{1} is continuous
by A2, JORDAN5A:27; :: thesis: verum

set c = the carrier of T;

for q being Point of T holds f . q <> 0

proof

then consider H being Function of T,R^1 such that
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;dom f = the carrier of T by FUNCT_2:def 1;

hence f . q <> 0 ; :: thesis: verum

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) "

dom h =
the carrier of T
by FUNCT_2:def 1
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;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

.= (dom f) \ (f " {0}) by FUNCT_2:def 1 ;

then h = f ^ by A3, RFUNCT_1:def 2;

hence for b

b