for n being non zero Nat holds MeasurableRectangle (ProductRightOpenIntervals n) = Product (n,the_set_of_all_right_open_real_bounded_intervals)