:: deftheorem Def5 defines TIMES TOPREALC:def 5 :
for n being Nat
for b₂ being Function of [:(TOP-REAL n),(TOP-REAL n):],(TOP-REAL n) holds
( b₂ = TIMES n iff for x, y being Point of (TOP-REAL n) holds b₂ . (x,y) = x (#) y );