let n be non zero Nat; :: thesis: for X being non-empty n -element FinSequence
for S being cap-closed-yielding SemiringFamily of X holds SemiringProduct S is cap-closed

let X be non-empty n -element FinSequence; :: thesis: for S being cap-closed-yielding SemiringFamily of X holds SemiringProduct S is cap-closed
let S be cap-closed-yielding SemiringFamily of X; :: thesis:
reconsider SP = SemiringProduct S as Subset-Family of () by Thm20;
defpred S1[ non zero Nat] means for X being non-empty \$1 -element FinSequence
for S being cap-closed-yielding SemiringFamily of X holds SemiringProduct S is cap-closed semiring_of_sets of ();
A1: S1 by Thm34;
A2: now :: thesis: for n being non zero Nat st S1[n] holds
S1[n + 1]
let n be non zero Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A3: S1[n] ; :: thesis: S1[n + 1]
now :: thesis: for X being non-empty n + 1 -element FinSequence
for S being cap-closed-yielding SemiringFamily of X holds SemiringProduct S is cap-closed semiring_of_sets of ()
let X be non-empty n + 1 -element FinSequence; :: thesis: for S being cap-closed-yielding SemiringFamily of X holds SemiringProduct S is cap-closed semiring_of_sets of ()
let S be cap-closed-yielding SemiringFamily of X; :: thesis:
reconsider SPS = SemiringProduct S as Subset-Family of () 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
.= (len Xq) + 1 by FINSEQ_1:39 ;
then A5: len Xq = n by ;
reconsider Xn = Xq as n -element FinSequence by ;
rng Xn c= rng X by ;
then A7: not {} in rng Xn ;
reconsider Xn = Xn as non-empty n -element FinSequence by ;
reconsider X1 = <*xq*> as 1 -element FinSequence ;
rng X1 c= rng X by ;
then A9: not {} in rng X1 ;
reconsider X1 = X1 as non-empty 1 -element FinSequence by ;
consider Sq being FinSequence, sq being object such that
A10: S = Sq ^ <*sq*> by FINSEQ_1:46;
len S = (len Sq) + (len <*sq*>) by
.= (len Sq) + 1 by FINSEQ_1:39 ;
then len Sq = n by ;
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:
A13: for i being Nat st i in Seg n holds
Sn . i is cap-closed semiring_of_sets of (Xn . i)
proof
let i be Nat; :: thesis: ( i in Seg n implies Sn . i is cap-closed semiring_of_sets of (Xn . i) )
assume A14: i in Seg n ; :: thesis: Sn . i is cap-closed 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 ;
then ( X . i = Xn . i & S . i = Sn . i ) by FINSEQ_1:64;
hence Sn . i is cap-closed semiring_of_sets of (Xn . i) by ; :: thesis: verum
end;
for i being Nat st i in Seg n holds
Sn . i is semiring_of_sets of (Xn . i) by A13;
then reconsider P = Sn as SemiringFamily of Xn by Def2;
P is cap-closed-yielding by A13;
hence Sn is cap-closed-yielding SemiringFamily of Xn ; :: thesis: verum
end;
then A16: ( Xn is non-empty & Sn is cap-closed-yielding SemiringFamily of Xn & SemiringProduct Sn is cap-closed semiring_of_sets of (product Xn) ) by A3;
A17: len X1 = 1 by FINSEQ_1:39;
then A18: X1 . 1 = X . (n + 1) by ;
len S1 = 1 by FINSEQ_1:39;
then A20: S1 . 1 = S . (n + 1) by ;
now :: thesis: ( X1 is non-empty & X1 . 1 = X . (n + 1) & S1 is cap-closed-yielding SemiringFamily of X1 )
thus X1 is non-empty ; :: thesis: ( X1 . 1 = X . (n + 1) & S1 is cap-closed-yielding SemiringFamily of X1 )
A23: n + 1 in Seg (n + 1) by FINSEQ_1:3;
A23a: now :: thesis: for i being Nat st i in Seg 1 holds
S1 . i is cap-closed semiring_of_sets of (X1 . i)
let i be Nat; :: thesis: ( i in Seg 1 implies S1 . i is cap-closed semiring_of_sets of (X1 . i) )
assume i in Seg 1 ; :: thesis: S1 . i is cap-closed semiring_of_sets of (X1 . i)
then i = 1 by ;
hence S1 . i is cap-closed semiring_of_sets of (X1 . i) by ; :: thesis: verum
end;
A23b: for i being Nat st i in Seg 1 holds
S1 . i is semiring_of_sets of (X1 . i) by A23a;
reconsider P = S1 as SemiringFamily of X1 by ;
for i being Nat st i in Seg 1 holds
P . i is cap-closed by A23a;
hence ( X1 . 1 = X . (n + 1) & S1 is cap-closed-yielding SemiringFamily of X1 ) by ; :: thesis: verum
end;
then A24: ( S1 is cap-closed-yielding SemiringFamily of X1 & SemiringProduct S1 is cap-closed semiring_of_sets of (product X1) ) by Thm34;
thus SemiringProduct S is cap-closed semiring_of_sets of () by A16, A24, Thm36, A10, A4; :: thesis: verum
end;
hence S1[n + 1] ; :: thesis: verum
end;
for n being non zero Nat holds S1[n] from NAT_1:sch 10(A1, A2);
hence SemiringProduct S is cap-closed ; :: thesis: verum