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_{1}[ 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}[1]
by Thm28;

_{1}[n]
from NAT_1:sch 10(A1, A2);

hence SemiringProduct S is semiring_of_sets of (product X) ; :: thesis: verum

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

for S being SemiringFamily of X holds SemiringProduct S is semiring_of_sets of (product X);

A1: S

A2: now :: thesis: for n being non zero Nat st S_{1}[n] holds

S_{1}[n + 1]

for n being non zero Nat holds SS

let n be non zero Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A3: S_{1}[n]
; :: thesis: S_{1}[n + 1]

_{1}[n + 1]
; :: thesis: verum

end;assume A3: S

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)

hence
Sfor 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;

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;

hence SemiringProduct S is semiring_of_sets of (product X) by A16, Thm31, A4, A10; :: thesis: verum

end;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

end;

then A16:
( Xn is non-empty & Sn is SemiringFamily of Xn & SemiringProduct Sn is semiring_of_sets of (product Xn) )
by A3;now :: thesis: for i being Nat st i in Seg n holds

Sn . i is semiring_of_sets of (Xn . i)

hence
Sn is SemiringFamily of Xn
by Def2; :: thesis: verumSn . 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;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

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 )

then
( S1 is SemiringFamily of X1 & SemiringProduct S1 is semiring_of_sets of (product X1) )
by Thm28;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;

end;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)

hence
( X1 . 1 = X . (n + 1) & S1 is SemiringFamily of X1 )
by A4, A12, A17, FINSEQ_1:65, Def2; :: thesis: verumS1 . 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;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

hence SemiringProduct S is semiring_of_sets of (product X) by A16, Thm31, A4, A10; :: thesis: verum

hence SemiringProduct S is semiring_of_sets of (product X) ; :: thesis: verum