for n being non zero Nat holds MeasurableRectangle (ProductLeftOpenIntervals n) is Semiring of (REAL n)