theorem Thm32: :: SRINGS_4:33

for n being non zero Nat
for X being non-empty b₁ -element FinSequence
for S being SemiringFamily of X holds SemiringProduct S is semiring_of_sets of (product X)