theorem Th30: :: SRINGS_5:34

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