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 SemialgebraFamily of Xn
for S1 being SemialgebraFamily of X1 holds SemiringProduct (Sn ^ S1) is semialgebra_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 SemialgebraFamily of Xn
for S1 being SemialgebraFamily of X1 holds SemiringProduct (Sn ^ S1) is semialgebra_of_sets of product (Xn ^ X1)
let X1 be non-empty 1 -element FinSequence; :: thesis: for Sn being SemialgebraFamily of Xn
for S1 being SemialgebraFamily of X1 holds SemiringProduct (Sn ^ S1) is semialgebra_of_sets of product (Xn ^ X1)
let Sn be SemialgebraFamily of Xn; :: thesis: for S1 being SemialgebraFamily of X1 holds SemiringProduct (Sn ^ S1) is semialgebra_of_sets of product (Xn ^ X1)
let S1 be SemialgebraFamily of X1; :: thesis: SemiringProduct (Sn ^ S1) is semialgebra_of_sets of product (Xn ^ X1)
A1: ( SemiringProduct Sn is semialgebra_of_sets of product Xn & SemiringProduct S1 is semialgebra_of_sets of product X1 ) by Th15;
reconsider S12 = { [:s1,s2:] where s1 is Element of SemiringProduct Sn, s2 is Element of SemiringProduct S1 : verum } as semialgebra_of_sets of [:(product Xn),(product X1):] by A1, Th14;
( SemiringProduct Sn is cap-closed semiring_of_sets of (product Xn) & SemiringProduct S1 is cap-closed semiring_of_sets of (product X1) ) by SRINGS_4:38;
then A5: SemiringProduct (Sn ^ S1) is cap-closed semiring_of_sets of (product (Xn ^ X1)) by SRINGS_4:37;
then A6: SemiringProduct (Sn ^ S1) is semi-diff-closed by SRINGS_3:10;
A11: ( dom Xn = dom Sn & dom X1 = dom S1 ) by SRINGS_4:18;
then A8: ( len Xn = len Sn & len X1 = len S1 ) by FINSEQ_3:29;
( len (Xn ^ X1) = (len Xn) + (len X1) & len (Sn ^ S1) = (len Sn) + (len S1) ) by FINSEQ_1:22;
then A7: dom (Xn ^ X1) = dom (Sn ^ S1) by A8, FINSEQ_3:29;
now :: thesis: for x being object st x in dom (Sn ^ S1) holds
(Xn ^ X1) . x in (Sn ^ S1) . x
let x be object ; :: thesis: ( x in dom (Sn ^ S1) implies (Xn ^ X1) . b1 in (Sn ^ S1) . b1 )
assume A9: x in dom (Sn ^ S1) ; :: thesis: (Xn ^ X1) . b1 in (Sn ^ S1) . b1
per cases ( x in dom Sn or ex k being Nat st
( k in dom S1 & x = (len Sn) + k ) ) by A9, FINSEQ_1:25;
suppose A10: x in dom Sn ; :: thesis: (Xn ^ X1) . b1 in (Sn ^ S1) . b1
then x in Seg n by FINSEQ_1:89;
then Xn . x in Sn . x by Th11;
then (Xn ^ X1) . x in Sn . x by A10, A11, FINSEQ_1:def 7;
hence (Xn ^ X1) . x in (Sn ^ S1) . x by A10, FINSEQ_1:def 7; :: thesis: verum
end;
suppose ex k being Nat st
( k in dom S1 & x = (len Sn) + k ) ; :: thesis: (Xn ^ X1) . b1 in (Sn ^ S1) . b1
then consider k being Nat such that
A12: ( k in dom S1 & x = (len Sn) + k ) ;
k in Seg 1 by A12, FINSEQ_1:89;
then X1 . k in S1 . k by Th11;
then (Xn ^ X1) . x in S1 . k by A12, A11, A8, FINSEQ_1:def 7;
hence (Xn ^ X1) . x in (Sn ^ S1) . x by A12, FINSEQ_1:def 7; :: thesis: verum
end;
end;
end;
then Xn ^ X1 in product (Sn ^ S1) by A7, CARD_3:9;
then product (Xn ^ X1) in SemiringProduct (Sn ^ S1) by SRINGS_4:def 4;
hence SemiringProduct (Sn ^ S1) is semialgebra_of_sets of product (Xn ^ X1) by A5, A6, SRINGS_3:def 6; :: thesis: verum