:: deftheorem Def5 defines R^1-TIMES TOPALG_7:def 5 :
for b₁ being Function of [:R^1,R^1:],R^1 holds
( b₁ = R^1-TIMES iff for x, y being Point of R^1 holds b₁ . (x,y) = x * y );