let X be non-empty 1 -element FinSequence; for S being SemialgebraFamily of X holds { (product <*s*>) where s is Element of S . 1 : verum } is semialgebra_of_sets of { <*x*> where x is Element of X . 1 : verum }
let S be SemialgebraFamily of X; { (product <*s*>) where s is Element of S . 1 : verum } is semialgebra_of_sets of { <*x*> where x is Element of X . 1 : verum }
set S1 = { (product <*s*>) where s is Element of S . 1 : verum } ;
set X1 = { <*x*> where x is Element of X . 1 : verum } ;
A1:
1 in Seg 1
;
then
X . 1 in S . 1
by Th11;
then A3:
product <*(X . 1)*> in { (product <*s*>) where s is Element of S . 1 : verum }
;
{ (product <*s*>) where s is Element of S . 1 : verum } is cap-closed semiring_of_sets of { <*x*> where x is Element of X . 1 : verum }
by SRINGS_4:34;
then A5:
{ (product <*s*>) where s is Element of S . 1 : verum } is with_empty_element cap-closed semi-diff-closed Subset-Family of { <*x*> where x is Element of X . 1 : verum }
by SRINGS_3:10;
1 in dom X
by A1, FINSEQ_1:89;
then
product <*(X . 1)*> = { <*y*> where y is Element of X . 1 : verum }
by SRINGS_4:24;
hence
{ (product <*s*>) where s is Element of S . 1 : verum } is semialgebra_of_sets of { <*x*> where x is Element of X . 1 : verum }
by A3, A5, SRINGS_3:def 6; verum