let n be non zero Nat; :: thesis:
let X be non-empty n -element FinSequence; :: thesis:
let S be SemialgebraFamily of X; :: thesis:
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:

let k be non zero Nat; :: thesis:
assume S₁[k] ; :: thesis:

let Xn1 be non-empty k + 1 -element FinSequence; :: thesis:
let Sn1 be SemialgebraFamily of Xn1; :: thesis:
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;

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

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:

end;

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

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: