let n be non zero Nat; :: thesis: MeasurableRectangle (ProductLeftOpenIntervals n) is Semiring of (REAL n)
MeasurableRectangle (ProductLeftOpenIntervals n) is Semiring of (product (ProductREAL n)) by SRINGS_4:40;
hence MeasurableRectangle (ProductLeftOpenIntervals n) is Semiring of (REAL n) by Th7; :: thesis: verum