consider H being Function of T,R^1 such that

A7: for p being Point of T

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

H . p = r1 * r2 and

A8: H is continuous by JGRAPH_2:25;

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

A9: 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) by FUNCT_2:def 1 ;

for c being object st c in dom h holds

h . c = (f . c) * (g . c) by A7;

then h = f (#) g by A9, VALUED_1:def 4;

hence for b_{1} being RealMap of T st b_{1} = f (#) g holds

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

A7: for p being Point of T

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

H . p = r1 * r2 and

A8: H is continuous by JGRAPH_2:25;

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

A9: 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) by FUNCT_2:def 1 ;

for c being object st c in dom h holds

h . c = (f . c) * (g . c) by A7;

then h = f (#) g by A9, VALUED_1:def 4;

hence for b

b