let X1, X2 be set ; :: thesis: for S1 being Semiring of X1
for S2 being Semiring of X2 holds { [:A,B:] where A is Element of S1, B is Element of S2 : verum } is Semiring of [:X1,X2:]
let S1 be Semiring of X1; :: thesis: for S2 being Semiring of X2 holds { [:A,B:] where A is Element of S1, B is Element of S2 : verum } is Semiring of [:X1,X2:]
let S2 be Semiring of X2; :: thesis: { [:A,B:] where A is Element of S1, B is Element of S2 : verum } is Semiring of [:X1,X2:]
A1: S1 is semiring_of_sets of X1 by SRINGS_3:9;
S2 is diff-c=-finite-partition-closed by SRINGS_3:9;
then { [:A,B:] where A is Element of S1, B is Element of S2 : verum } is cap-closed semiring_of_sets of [:X1,X2:] by A1, SRINGS_4:36;
hence { [:A,B:] where A is Element of S1, B is Element of S2 : verum } is Semiring of [:X1,X2:] by SRINGS_3:10; :: thesis: verum