let X1, X2 be set ; :: thesis: for S1 being semiring_of_sets of X1
for S2 being semiring_of_sets of X2 holds { [:s1,s2:] where s1 is Element of S1, s2 is Element of S2 : verum } is semiring_of_sets of [:X1,X2:]
let S1 be semiring_of_sets of X1; :: thesis: for S2 being semiring_of_sets of X2 holds { [:s1,s2:] where s1 is Element of S1, s2 is Element of S2 : verum } is semiring_of_sets of [:X1,X2:]
let S2 be semiring_of_sets of X2; :: thesis: { [:s1,s2:] where s1 is Element of S1, s2 is Element of S2 : verum } is semiring_of_sets of [:X1,X2:]
set S = { s where s is Subset of [:X1,X2:] : ex x1, x2 being set st
( x1 in S1 & x2 in S2 & s = [:x1,x2:] ) } ;
{ s where s is Subset of [:X1,X2:] : ex x1, x2 being set st
( x1 in S1 & x2 in S2 & s = [:x1,x2:] ) } is semiring_of_sets of [:X1,X2:] by SRINGS_2:7;
hence { [:s1,s2:] where s1 is Element of S1, s2 is Element of S2 : verum } is semiring_of_sets of [:X1,X2:] by SRINGS_2:2; :: thesis: verum