theorem Thm28: :: SRINGS_4:29

for X being non-empty 1 -element FinSequence
for S being SemiringFamily of X holds SemiringProduct S is semiring_of_sets of (product X)