let n be non zero Nat; :: thesis: for X being non-empty n -element FinSequence
for S being SemialgebraFamily of X holds SemiringProduct S is semialgebra_of_sets of product X
let X be non-empty n -element FinSequence; :: thesis: for S being SemialgebraFamily of X holds SemiringProduct S is semialgebra_of_sets of product X
let S be SemialgebraFamily of X; :: thesis: SemiringProduct S is semialgebra_of_sets of product X
defpred S₁[ non zero Nat] means for X being non-empty $1 -element FinSequence
for S being SemialgebraFamily of X holds SemiringProduct S is semialgebra_of_sets of product X;
A1: S₁[1] by Th13;

A2: now :: thesis: for k being non zero Nat st S₁[k] holds
S₁[k + 1]

let k be non zero Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume S₁[k] ; :: thesis: S₁[k + 1]

now :: thesis: for Xn1 being non-empty k + 1 -element FinSequence
for Sn1 being SemialgebraFamily of Xn1 holds SemiringProduct Sn1 is semialgebra_of_sets of product Xn1

let Xn1 be non-empty k + 1 -element FinSequence; :: thesis: for Sn1 being SemialgebraFamily of Xn1 holds SemiringProduct Sn1 is semialgebra_of_sets of product Xn1
let Sn1 be SemialgebraFamily of Xn1; :: thesis: SemiringProduct Sn1 is semialgebra_of_sets of product Xn1
A3: SemiringProduct Sn1 is cap-closed semiring_of_sets of (product Xn1) by SRINGS_4:38;
then A4: SemiringProduct Sn1 is semi-diff-closed by SRINGS_3:10;
A6: dom Xn1 = dom Sn1 by SRINGS_4:18;

now :: thesis: for x being object st x in dom Sn1 holds
Xn1 . x in Sn1 . x

let x be object ; :: thesis: ( x in dom Sn1 implies Xn1 . x in Sn1 . x )
assume x in dom Sn1 ; :: thesis: Xn1 . x in Sn1 . x
then x in Seg (k + 1) by FINSEQ_1:89;
hence Xn1 . x in Sn1 . x by Th11; :: thesis: verum

end;

then Xn1 in product Sn1 by A6, CARD_3:9;
then product Xn1 in SemiringProduct Sn1 by SRINGS_4:def 4;
hence SemiringProduct Sn1 is semialgebra_of_sets of product Xn1 by A3, A4, SRINGS_3:def 6; :: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: verum

end;

for k being non zero Nat holds S₁[k] from NAT_1:sch 10(A1, A2);
hence SemiringProduct S is semialgebra_of_sets of product X ; :: thesis: verum