for x, y being Point of I[01] holds I[01]-TIMES . (x,y) = x * y