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