for X being non-empty 1 -element FinSequence
for S being SemialgebraFamily of X holds SemiringProduct S is semialgebra_of_sets of product X