let X be non-empty 1 -element FinSequence; :: thesis: for S being SemiringFamily of X holds SemiringProduct S is semiring_of_sets of (product X)
let S be SemiringFamily of X; :: thesis: SemiringProduct S is semiring_of_sets of (product X)
set S1 = { (product <*s*>) where s is Element of S . 1 : verum } ;
set X1 = { <*x*> where x is Element of X . 1 : verum } ;
( { (product <*s*>) where s is Element of S . 1 : verum } = SemiringProduct S & { <*x*> where x is Element of X . 1 : verum } = product X ) by Thm21, Thm24;
hence SemiringProduct S is semiring_of_sets of (product X) by Thm27; :: thesis: verum