let X be non-empty 1 -element FinSequence; :: thesis: for S being cap-closed-yielding SemiringFamily of X holds { (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 }
let S be cap-closed-yielding SemiringFamily of X; :: thesis: { (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 }
( S is cap-closed-yielding SemiringFamily of X & 1 in Seg 1 ) by FINSEQ_1:3;
then A1: ( S . 1 is semiring_of_sets of (X . 1) & S . 1 is cap-closed ) by Def2, Def4;
set S1 = { (product <*s*>) where s is Element of S . 1 : verum } ;
set X1 = { <*x*> where x is Element of X . 1 : verum } ;
now :: thesis: for s1, s2 being set st s1 in { (product <*s*>) where s is Element of S . 1 : verum } & s2 in { (product <*s*>) where s is Element of S . 1 : verum } holds
s1 /\ s2 in { (product <*s*>) where s is Element of S . 1 : verum }
let s1, s2 be set ; :: thesis: ( s1 in { (product <*s*>) where s is Element of S . 1 : verum } & s2 in { (product <*s*>) where s is Element of S . 1 : verum } implies s1 /\ s2 in { (product <*s*>) where s is Element of S . 1 : verum } )
assume that
A2: s1 in { (product <*s*>) where s is Element of S . 1 : verum } and
A3: s2 in { (product <*s*>) where s is Element of S . 1 : verum } ; :: thesis: s1 /\ s2 in { (product <*s*>) where s is Element of S . 1 : verum }
consider t1 being Element of S . 1 such that
A4: s1 = product <*t1*> by A2;
consider t2 being Element of S . 1 such that
A5: s2 = product <*t2*> by A3;
A6: s1 /\ s2 = product <*(t1 /\ t2)*> by A4, A5, Thm25;
t1 /\ t2 is Element of S . 1 by A1;
hence s1 /\ s2 in { (product <*s*>) where s is Element of S . 1 : verum } by A6; :: thesis: verum
end;
then { (product <*s*>) where s is Element of S . 1 : verum } is cap-closed ;
hence { (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 Thm27; :: thesis: verum