theorem Thm36: :: SRINGS_4:37

for n being non zero Nat
for Xn being non-empty b₁ -element FinSequence
for X1 being non-empty 1 -element FinSequence
for Sn being cap-closed-yielding SemiringFamily of Xn
for S1 being cap-closed-yielding SemiringFamily of X1 st SemiringProduct Sn is cap-closed semiring_of_sets of (product Xn) & SemiringProduct S1 is cap-closed semiring_of_sets of (product X1) holds
SemiringProduct (Sn ^ S1) is cap-closed semiring_of_sets of (product (Xn ^ X1))