for n being non zero Nat
for Xn being non-empty b₁ -element FinSequence
for X1 being non-empty 1 -element FinSequence
for Sn being SemiringFamily of Xn
for S1 being SemiringFamily of X1 st SemiringProduct Sn is semiring_of_sets of (product Xn) & SemiringProduct S1 is semiring_of_sets of (product X1) holds
for S12 being Subset-Family of [:(product Xn),(product X1):] st S12 = { [:s1,s2:] where s1 is Element of SemiringProduct Sn, s2 is Element of SemiringProduct S1 : verum } holds
ex I being Function of [:(product Xn),(product X1):],(product (Xn ^ X1)) st
( I is one-to-one & I is onto & ( for x, y being FinSequence st x in product Xn & y in product X1 holds
I . (x,y) = x ^ y ) & I .: S12 = SemiringProduct (Sn ^ S1) )