let n be non zero Nat; :: thesis: for X being non-empty n -element FinSequence
for S being SemiringFamily of X holds SemiringProduct S is semiring_of_sets of (product X)
let X be non-empty n -element FinSequence; :: thesis: for S being SemiringFamily of X holds SemiringProduct S is semiring_of_sets of (product X)
let S be SemiringFamily of X; :: thesis: SemiringProduct S is semiring_of_sets of (product X)
reconsider SP = SemiringProduct S as Subset-Family of (product X) by Thm20;
defpred S₁[ non zero Nat] means for X being non-empty $1 -element FinSequence
for S being SemiringFamily of X holds SemiringProduct S is semiring_of_sets of (product X);
A1: S₁[1] by Thm28;

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

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

now :: thesis: for X being non-empty n + 1 -element FinSequence
for S being SemiringFamily of X holds SemiringProduct S is semiring_of_sets of (product X)

let X be non-empty n + 1 -element FinSequence; :: thesis: for S being SemiringFamily of X holds SemiringProduct S is semiring_of_sets of (product X)
let S be SemiringFamily of X; :: thesis: SemiringProduct S is semiring_of_sets of (product X)
reconsider SPS = SemiringProduct S as Subset-Family of (product X) by Thm20;
consider Xq being FinSequence, xq being object such that
A4: X = Xq ^ <*xq*> by FINSEQ_1:46;
len X = (len Xq) + (len <*xq*>) by A4, FINSEQ_1:22
.= (len Xq) + 1 by FINSEQ_1:39 ;
then A5: len Xq = n by XCMPLX_1:2, FINSEQ_3:153;
reconsider Xn = Xq as n -element FinSequence by A5, CARD_1:def 7;
rng Xn c= rng X by A4, FINSEQ_1:29;
then A7: not {} in rng Xn ;
reconsider Xn = Xn as non-empty n -element FinSequence by A7, RELAT_1:def 9;
reconsider X1 = <*xq*> as 1 -element FinSequence ;
rng X1 c= rng X by A4, FINSEQ_1:30;
then A9: not {} in rng X1 ;
reconsider X1 = X1 as non-empty 1 -element FinSequence by A9, RELAT_1:def 9;
consider Sq being FinSequence, sq being object such that
A10: S = Sq ^ <*sq*> by FINSEQ_1:46;
len S = (len Sq) + (len <*sq*>) by A10, FINSEQ_1:22
.= (len Sq) + 1 by FINSEQ_1:39 ;
then len Sq = n by FINSEQ_3:153, XCMPLX_1:2;
then reconsider Sn = Sq as n -element FinSequence by CARD_1:def 7;
reconsider S1 = <*sq*> as 1 -element FinSequence ;
Seg (n + 1) = (Seg n) \/ {(n + 1)} by FINSEQ_1:9;
then A11: Seg n c= Seg (n + 1) by XBOOLE_1:7;
A12: ( len Xn = n & len Sn = n ) by FINSEQ_3:153;

now :: thesis: Sn is SemiringFamily of Xn

now :: thesis: for i being Nat st i in Seg n holds
Sn . i is semiring_of_sets of (Xn . i)

let i be Nat; :: thesis: ( i in Seg n implies Sn . i is semiring_of_sets of (Xn . i) )
assume A14: i in Seg n ; :: thesis: Sn . i is semiring_of_sets of (Xn . i)
then ( i in Seg (len Xn) & i in Seg (len Sn) ) by FINSEQ_3:153;
then ( X . i = (Xn ^ X1) . i & S . i = (Sn ^ S1) . i & 1 <= i & i <= len Xn & i <= len Sn ) by A4, A10, FINSEQ_1:1;
then ( X . i = Xn . i & S . i = Sn . i ) by FINSEQ_1:64;
hence Sn . i is semiring_of_sets of (Xn . i) by A14, A11, Def2; :: thesis: verum

end;

hence Sn is SemiringFamily of Xn by Def2; :: thesis: verum

end;

then A16: ( Xn is non-empty & Sn is SemiringFamily of Xn & SemiringProduct Sn is semiring_of_sets of (product Xn) ) by A3;
A17: len X1 = 1 by FINSEQ_1:39;
then A18: X1 . 1 = X . (n + 1) by FINSEQ_1:65, A4, A12;
len S1 = 1 by FINSEQ_1:39;
then A20: S1 . 1 = S . (n + 1) by FINSEQ_1:65, A12, A10;

now :: thesis: ( X1 is non-empty & X1 . 1 = X . (n + 1) & S1 is SemiringFamily of X1 )

thus X1 is non-empty ; :: thesis: ( X1 . 1 = X . (n + 1) & S1 is SemiringFamily of X1 )
A23: n + 1 in Seg (n + 1) by FINSEQ_1:3;

now :: thesis: for i being Nat st i in Seg 1 holds
S1 . i is semiring_of_sets of (X1 . i)

let i be Nat; :: thesis: ( i in Seg 1 implies S1 . i is semiring_of_sets of (X1 . i) )
assume i in Seg 1 ; :: thesis: S1 . i is semiring_of_sets of (X1 . i)
then i = 1 by TARSKI:def 1, FINSEQ_1:2;
hence S1 . i is semiring_of_sets of (X1 . i) by A23, A20, A18, Def2; :: thesis: verum

end;

hence ( X1 . 1 = X . (n + 1) & S1 is SemiringFamily of X1 ) by A4, A12, A17, FINSEQ_1:65, Def2; :: thesis: verum

end;

then ( S1 is SemiringFamily of X1 & SemiringProduct S1 is semiring_of_sets of (product X1) ) by Thm28;
hence SemiringProduct S is semiring_of_sets of (product X) by A16, Thm31, A4, A10; :: thesis: verum

end;

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

end;

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