for n being non zero Nat
for X being non-empty b₁ -element FinSequence
for S being cap-closed-yielding SemiringFamily of X holds SemiringProduct S is cap-closed semiring_of_sets of (product X) by Thm32;