for X1, X2 being set
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:]