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 }