reconsider F = f, G = g 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 g . q <> 0

A1: for p being Point of T

for r1, r2 being Real st F . p = r1 & G . p = r2 holds

H . p = r1 / r2 and

A2: H is continuous by JGRAPH_2:27;

reconsider h = H as RealMap of T by TOPMETR:17;

.= the carrier of T /\ (dom g) by FUNCT_2:def 1

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

then h = f / g by A3, RFUNCT_1:def 1;

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

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

set c = the carrier of T;

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

proof

then consider H being Function of T,R^1 such that
let q be Point of T; :: thesis: g . q <> 0

dom g = the carrier of T by FUNCT_2:def 1;

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

end;dom g = the carrier of T by FUNCT_2:def 1;

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

A1: for p being Point of T

for r1, r2 being Real st F . p = r1 & G . p = r2 holds

H . p = r1 / r2 and

A2: H is continuous by JGRAPH_2:27;

reconsider h = H as RealMap of T by TOPMETR:17;

A3: now :: thesis: for c being object st c in dom h holds

h . c = (f . c) * ((g . c) ")

dom h =
the carrier of T /\ the carrier of T
by FUNCT_2:def 1
h . c = (f . c) * ((g . c) ")

let c be object ; :: 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;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

.= the carrier of T /\ (dom g) by FUNCT_2:def 1

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

then h = f / g by A3, RFUNCT_1:def 1;

hence for b

b