let x, y be Point of I[01]; :: thesis: I[01]-TIMES . (x,y) = x * y
( x is Point of R^1 & y is Point of R^1 ) by PRE_TOPC:25;
hence x * y = R^1-TIMES . (x,y) by Def5
.= I[01]-TIMES . (x,y) by FUNCT_1:49, ZFMISC_1:87, BORSUK_1:40 ;
:: thesis: verum