let X be non-empty 1 -element FinSequence; :: thesis: for S being SemialgebraFamily of X holds SemiringProduct S is semialgebra_of_sets of product X
let S be SemialgebraFamily of X; :: thesis: SemiringProduct S is semialgebra_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 SRINGS_4:23, SRINGS_4:25;
hence SemiringProduct S is semialgebra_of_sets of product X by Th12; :: thesis: verum