let F be Function of T,R^1; :: thesis: ( F = f (#) g implies F is continuous )

assume A4: F = f (#) g ; :: thesis: F is continuous

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

A5: for p being Point of T

for r1, r2 being Real st f . p = r1 & g . p = r2 holds

h . p = r1 * r2 and

A6: h is continuous by JGRAPH_2:25;

F = h

assume A4: F = f (#) g ; :: thesis: F is continuous

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

A5: for p being Point of T

for r1, r2 being Real st f . p = r1 & g . p = r2 holds

h . p = r1 * r2 and

A6: h is continuous by JGRAPH_2:25;

F = h

proof

hence
F is continuous
by A6; :: thesis: verum
let x be Point of T; :: according to FUNCT_2:def 8 :: thesis: F . x = h . x

thus F . x = (f . x) * (g . x) by A4, VALUED_1:5

.= h . x by A5 ; :: thesis: verum

end;thus F . x = (f . x) * (g . x) by A4, VALUED_1:5

.= h . x by A5 ; :: thesis: verum