let X be non-empty 1 -element FinSequence; :: thesis: for S being cap-closed-yielding SemiringFamily of X holds SemiringProduct S is cap-closed semiring_of_sets of (product X)

let S be cap-closed-yielding SemiringFamily of X; :: thesis: SemiringProduct S is cap-closed 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 cap-closed semiring_of_sets of (product X) by Thm33; :: thesis: verum

let S be cap-closed-yielding SemiringFamily of X; :: thesis: SemiringProduct S is cap-closed 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 cap-closed semiring_of_sets of (product X) by Thm33; :: thesis: verum