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;

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)

hence
R^1-TIMES is continuous
by A2, Lm1, BINOP_1:2; :: thesis: verumlet 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;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