theorem Thm27: :: SRINGS_4:28

for X being non-empty 1 -element FinSequence
for S being SemiringFamily of X holds { (product <*s*>) where s is Element of S . 1 : verum } is semiring_of_sets of { <*x*> where x is Element of X . 1 : verum }