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 :: thesis: 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; :: thesis: 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) ; :: thesis: verum

end;

hence R^1-TIMES is continuous by A2, Lm1, BINOP_1:2; :: thesis: verum