theorem Thm24: :: SRINGS_4:25

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