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 SemialgebraFamily of Xn
for S1 being SemialgebraFamily of X1 holds SemiringProduct (Sn ^ S1) is semialgebra_of_sets of product (Xn ^ X1)