let n be non zero Nat; :: thesis: for X being non-empty n -element FinSequence

for S being ClassicalSemiringFamily of X holds MeasurableRectangle S is cap-closed with_empty_element semi-diff-closed Subset-Family of (product X)

let X be non-empty n -element FinSequence; :: thesis: for S being ClassicalSemiringFamily of X holds MeasurableRectangle S is cap-closed with_empty_element semi-diff-closed Subset-Family of (product X)

let S be ClassicalSemiringFamily of X; :: thesis: MeasurableRectangle S is cap-closed with_empty_element semi-diff-closed Subset-Family of (product X)

reconsider S1 = S as cap-closed-yielding SemiringFamily of X by Thm38;

SemiringProduct S1 is cap-closed cap-finite-partition-closed diff-finite-partition-closed with_empty_element Subset-Family of (product X) by Thm32;

hence MeasurableRectangle S is cap-closed with_empty_element semi-diff-closed Subset-Family of (product X) by SRINGS_3:10; :: thesis: verum

for S being ClassicalSemiringFamily of X holds MeasurableRectangle S is cap-closed with_empty_element semi-diff-closed Subset-Family of (product X)

let X be non-empty n -element FinSequence; :: thesis: for S being ClassicalSemiringFamily of X holds MeasurableRectangle S is cap-closed with_empty_element semi-diff-closed Subset-Family of (product X)

let S be ClassicalSemiringFamily of X; :: thesis: MeasurableRectangle S is cap-closed with_empty_element semi-diff-closed Subset-Family of (product X)

reconsider S1 = S as cap-closed-yielding SemiringFamily of X by Thm38;

SemiringProduct S1 is cap-closed cap-finite-partition-closed diff-finite-partition-closed with_empty_element Subset-Family of (product X) by Thm32;

hence MeasurableRectangle S is cap-closed with_empty_element semi-diff-closed Subset-Family of (product X) by SRINGS_3:10; :: thesis: verum