theorem Th08: :: MEASUR10:10

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