let n be non zero Nat; :: thesis: for Xn being non-empty n -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
SemiringProduct (Sn ^ S1) is semiring_of_sets of (product (Xn ^ X1))
let Xn be non-empty n -element FinSequence; :: thesis: 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
SemiringProduct (Sn ^ S1) is semiring_of_sets of (product (Xn ^ X1))
let X1 be non-empty 1 -element FinSequence; :: thesis: 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
SemiringProduct (Sn ^ S1) is semiring_of_sets of (product (Xn ^ X1))
let Sn be SemiringFamily of Xn; :: thesis: 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
SemiringProduct (Sn ^ S1) is semiring_of_sets of (product (Xn ^ X1))
let S1 be SemiringFamily of X1; :: thesis: ( SemiringProduct Sn is semiring_of_sets of (product Xn) & SemiringProduct S1 is semiring_of_sets of (product X1) implies SemiringProduct (Sn ^ S1) is semiring_of_sets of (product (Xn ^ X1)) )
assume that
A1: SemiringProduct Sn is semiring_of_sets of (product Xn) and
A2: SemiringProduct S1 is semiring_of_sets of (product X1) ; :: thesis: SemiringProduct (Sn ^ S1) is semiring_of_sets of (product (Xn ^ X1))
reconsider S12 = { [:s1,s2:] where s1 is Element of SemiringProduct Sn, s2 is Element of SemiringProduct S1 : verum } as semiring_of_sets of [:(product Xn),(product X1):] by A1, A2, Thm29;
consider I being Function of [:(product Xn),(product X1):],(product (Xn ^ X1)) such that
A3: I is one-to-one and
I is onto and
for x, y being FinSequence st x in product Xn & y in product X1 holds
I . (x,y) = x ^ y and
A4: I .: S12 = SemiringProduct (Sn ^ S1) by A1, A2, Thm30;
thus SemiringProduct (Sn ^ S1) is semiring_of_sets of (product (Xn ^ X1)) by A3, A4, Thm11, Thm12; :: thesis: verum