theorem :: SRINGS_2:7

for X1, X2 being set
for S1 being semiring_of_sets of X1
for S2 being semiring_of_sets of X2 holds { 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:]