reconsider f1 = pr1 ( the carrier of R^1, the carrier of R^1) as continuous Function of [:R^1,R^1:],R^1 by YELLOW12:39;
reconsider f2 = pr2 ( the carrier of R^1, the carrier of R^1) as continuous Function of [:R^1,R^1:],R^1 by YELLOW12:40;
consider g being Function of [:R^1,R^1:],R^1 such that
A1:
for p being Point of [:R^1,R^1:]
for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds
g . p = r1 * r2
and
A2:
g is continuous
by JGRAPH_2:25;
now for a, b being Point of R^1 holds R^1-TIMES . (a,b) = g . (a,b)let a,
b be
Point of
R^1;
R^1-TIMES . (a,b) = g . (a,b)A3:
(
f1 . (
a,
b)
= a &
f2 . (
a,
b)
= b )
by FUNCT_3:def 4, FUNCT_3:def 5;
thus R^1-TIMES . (
a,
b) =
a * b
by Def5
.=
g . [a,b]
by A1, A3
.=
g . (
a,
b)
;
verum end;
hence
R^1-TIMES is continuous
by A2, Lm1, BINOP_1:2; verum