let X be non-empty 1 -element FinSequence; :: thesis:
let S be SemiringFamily of X; :: thesis:
( S is SemiringFamily of X & 1 in Seg 1 ) by FINSEQ_1:3;
then A1: S . 1 is semiring_of_sets of (X . 1) by Def2;
set S1 = { (product <*s*>) where s is Element of S . 1 : verum } ;
set X1 = { <*x*> where x is Element of X . 1 : verum } ;

now :: thesis:

{ (product <*s*>) where s is Element of S . 1 : verum } c= bool { <*x*> where x is Element of X . 1 : verum }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A2: x in { (product <*s*>) where s is Element of S . 1 : verum } ; :: thesis:
then consider s0 being Element of S . 1 such that
A3: x = product <*s0*> ;

per cases ;

suppose A4: not s0 is empty ; :: thesis:

reconsider x1 = x as set by A2;
x1 c= { <*x*> where x is Element of X . 1 : verum }

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in x1 ; :: thesis:
then y in { <*a*> where a is Element of s0 : verum } by A3, A4, Thm23;
then consider a being Element of s0 such that
A6: y = <*a*> ;
A7: a in union (S . 1) by A4, A1, TARSKI:def 4;
union (S . 1) c= union (bool (X . 1)) by A1, ZFMISC_1:77;
then union (S . 1) c= X . 1 by ZFMISC_1:81;
hence y in { <*x*> where x is Element of X . 1 : verum } by A6, A7; :: thesis:

end;

hence x in bool { <*x*> where x is Element of X . 1 : verum } ; :: thesis:

end;

suppose A8: s0 is empty ; :: thesis:

product <*{}*> c= { <*x*> where x is Element of X . 1 : verum } ;
hence x in bool { <*x*> where x is Element of X . 1 : verum } by A8, A3; :: thesis:

end;

then reconsider S2 = { (product <*s*>) where s is Element of S . 1 : verum } as Subset-Family of { <*x*> where x is Element of X . 1 : verum } ;

now :: thesis:

Z: {} is Element of S . 1 by A1, SETFAM_1:def 8;
then A9: {} in { (product <*s*>) where s is Element of S . 1 : verum } by Thm22;
thus S2 is with_empty_element by Z, Thm22; :: thesis:

now :: thesis:

let s1, s2 be Element of S2; :: thesis:
assume A10: not s1 /\ s2 is empty ; :: thesis:
A11: ( s1 in { (product <*s*>) where s is Element of S . 1 : verum } & s2 in S2 ) by A9;
then consider sa1 being Element of S . 1 such that
A12: s1 = product <*sa1*> ;
consider sa2 being Element of S . 1 such that
A13: s2 = product <*sa2*> by A11;
A14: not sa1 /\ sa2 is empty by A12, A13, A10, Thm25, Thm22;
then consider ax being finite Subset of (S . 1) such that
A15: ax is a_partition of sa1 /\ sa2 by A1, SRINGS_1:def 1;
A16: not ax is empty by A14, A15;
set x = { (product <*t*>) where t is Element of ax : verum } ;

now :: thesis:

deffunc H₁( object ) -> set = product <*$1*>;
consider f being Function such that
A17: dom f = ax and
A18: for x being object st x in ax holds
f . x = H₁(x) from FUNCT_1:sch 3();
rng f = { (product <*t*>) where t is Element of ax : verum }

proof

now :: thesis:

hereby :: thesis:

let t be object ; :: thesis:
assume t in rng f ; :: thesis:
then consider q being object such that
A19: q in dom f and
A20: t = f . q by FUNCT_1:def 3;
t = H₁(q) by A17, A19, A20, A18;
hence t in { (product <*t*>) where t is Element of ax : verum } by A17, A19; :: thesis:

end;

let t be object ; :: thesis:
assume t in { (product <*t*>) where t is Element of ax : verum } ; :: thesis:
then consider u being Element of ax such that
A21: t = product <*u*> ;
f . u = H₁(u) by A18, A14, A15;
hence t in rng f by A21, A17, A14, A15, FUNCT_1:def 3; :: thesis:

end;

then ( { (product <*t*>) where t is Element of ax : verum } c= rng f & rng f c= { (product <*t*>) where t is Element of ax : verum } ) ;
hence rng f = { (product <*t*>) where t is Element of ax : verum } ; :: thesis:

end;

hence { (product <*t*>) where t is Element of ax : verum } is finite by A17, FINSET_1:8; :: thesis:
{ (product <*t*>) where t is Element of ax : verum } c= S2

proof

let t be object ; :: according to TARSKI:def 3 :: thesis:
assume t in { (product <*t*>) where t is Element of ax : verum } ; :: thesis:
then consider u being Element of ax such that
A22: t = product <*u*> ;
( u in ax & ax c= S . 1 ) by A16;
hence t in S2 by A22; :: thesis:

end;

hence { (product <*t*>) where t is Element of ax : verum } is Subset of S2 ; :: thesis:

now :: thesis:

A23: { (product <*t*>) where t is Element of ax : verum } c= bool (s1 /\ s2)

proof

let t be object ; :: according to TARSKI:def 3 :: thesis:
assume t in { (product <*t*>) where t is Element of ax : verum } ; :: thesis:
then consider u0 being Element of ax such that
A24: t = product <*u0*> ;
reconsider t1 = t as set by A24;

per cases ;

suppose A25: t1 is empty ; :: thesis:

{} c= s1 /\ s2 ;
hence t in bool (s1 /\ s2) by A25; :: thesis:

end;

suppose A26: not t1 is empty ; :: thesis:

then A28: t = { <*y*> where y is Element of u0 : verum } by A24, Thm22, Thm23;
t1 c= s1 /\ s2

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in t1 ; :: thesis:
then consider z being Element of u0 such that
A29: y = <*z*> by A28;
A30: product <*(sa1 /\ sa2)*> = { <*a*> where a is Element of sa1 /\ sa2 : verum } by A14, Thm23;
( u0 in ax & union ax = sa1 /\ sa2 ) by A16, A15, EQREL_1:def 4;
then z in sa1 /\ sa2 by A24, A26, Thm22, TARSKI:def 4;
then y in product <*(sa1 /\ sa2)*> by A29, A30;
hence y in s1 /\ s2 by A12, A13, Thm25; :: thesis:

end;

hence t in bool (s1 /\ s2) ; :: thesis:

end;

hence { (product <*t*>) where t is Element of ax : verum } is Subset-Family of (s1 /\ s2) ; :: thesis:

now :: thesis:

hereby :: thesis:

let a be object ; :: thesis:
assume a in union { (product <*t*>) where t is Element of ax : verum } ; :: thesis:
then consider b being set such that
A31: a in b and
A32: b in { (product <*t*>) where t is Element of ax : verum } by TARSKI:def 4;
thus a in s1 /\ s2 by A31, A32, A23; :: thesis:

end;

let a be object ; :: thesis:
assume a in s1 /\ s2 ; :: thesis:
then A33: a in product <*(sa1 /\ sa2)*> by A12, A13, Thm25;
product <*(sa1 /\ sa2)*> = { <*u*> where u is Element of sa1 /\ sa2 : verum } by A14, Thm23;
then consider b being Element of sa1 /\ sa2 such that
A34: a = <*b*> by A33;
( b in sa1 /\ sa2 & union ax = sa1 /\ sa2 ) by A14, A15, EQREL_1:def 4;
then consider d being set such that
A35: ( b in d & d in ax ) by TARSKI:def 4;
A36: product <*d*> = { <*u*> where u is Element of d : verum } by A35, Thm23;
( <*b*> in product <*d*> & product <*d*> in { (product <*t*>) where t is Element of ax : verum } ) by A35, A36;
hence a in union { (product <*t*>) where t is Element of ax : verum } by A34, TARSKI:def 4; :: thesis:

end;

then ( union { (product <*t*>) where t is Element of ax : verum } c= s1 /\ s2 & s1 /\ s2 c= union { (product <*t*>) where t is Element of ax : verum } ) ;
hence union { (product <*t*>) where t is Element of ax : verum } = s1 /\ s2 ; :: thesis:

hereby :: thesis:

let A be Subset of (s1 /\ s2); :: thesis:
assume A in { (product <*t*>) where t is Element of ax : verum } ; :: thesis:
then consider a being Element of ax such that
A37: A = product <*a*> ;
A38: a in ax by A16;
A39: A = { <*u*> where u is Element of a : verum } by A14, A15, A37, Thm23;
consider b being object such that
A40: b in a by A14, A15, XBOOLE_0:def 1;
<*b*> in A by A39, A40;
hence A <> {} ; :: thesis:
let B be Subset of (s1 /\ s2); :: thesis:
assume B in { (product <*t*>) where t is Element of ax : verum } ; :: thesis:
then consider b being Element of ax such that
A41: B = product <*b*> ;
A42: b in ax by A16;
( a misses b implies A misses B ) by A37, A41, Thm25, Thm22;
hence ( A = B or A misses B ) by A42, A38, A15, EQREL_1:def 4, A37, A41; :: thesis:

end;

hence { (product <*t*>) where t is Element of ax : verum } is a_partition of s1 /\ s2 by EQREL_1:def 4; :: thesis:

end;

hence ex x being finite Subset of S2 st x is a_partition of s1 /\ s2 ; :: thesis:

end;

hence S2 is cap-finite-partition-closed ; :: thesis:

now :: thesis:

let s1, s2 be Element of S2; :: thesis:
assume A44: s2 c= s1 ; :: thesis:

per cases ;

suppose A45: s1 \ s2 is empty ; :: thesis:

now :: thesis:

{} c= S2 ;
hence {} is finite Subset of S2 ; :: thesis:
thus {} is a_partition of {} by EQREL_1:45; :: thesis:

end;

hence ex x being finite Subset of S2 st x is a_partition of s1 \ s2 by A45; :: thesis:

end;

suppose A46: ( not s1 \ s2 is empty & s2 is empty ) ; :: thesis:

now :: thesis:

{s1} c= S2

proof

let t be object ; :: according to TARSKI:def 3 :: thesis:
assume t in {s1} ; :: thesis:
then t = s1 by TARSKI:def 1;
hence t in S2 by A9; :: thesis:

end;

hence {s1} is finite Subset of S2 ; :: thesis:
thus {s1} is a_partition of s1 by A46, EQREL_1:39; :: thesis:

end;

hence ex x being finite Subset of S2 st x is a_partition of s1 \ s2 by A46; :: thesis:

end;

suppose A47: ( not s1 \ s2 is empty & not s2 is empty ) ; :: thesis:

A48: ( s1 in { (product <*s*>) where s is Element of S . 1 : verum } & s2 in S2 ) by A9;
then consider sa1 being Element of S . 1 such that
A49: s1 = product <*sa1*> ;
consider sa2 being Element of S . 1 such that
A50: s2 = product <*sa2*> by A48;
A51: not sa1 is empty by A47, A49;
A52: product <*sa1*> = { <*u*> where u is Element of sa1 : verum } by A47, A49, Thm22, Thm23;
A53: product <*sa2*> = { <*u*> where u is Element of sa2 : verum } by A47, A50, Thm22, Thm23;
sa2 c= sa1

proof

assume not sa2 c= sa1 ; :: thesis:
then consider a being object such that
A54: a in sa2 and
A55: not a in sa1 ;
<*a*> in s2 by A50, A54, A53;
then <*a*> in product <*sa1*> by A44, A49;
then consider a0 being Element of sa1 such that
A56: <*a*> = <*a0*> by A52;
a = a0 by A56, FINSEQ_1:76;
hence contradiction by A51, A55; :: thesis:

end;

then consider ax being finite Subset of (S . 1) such that
A57: ax is a_partition of sa1 \ sa2 by A1, SRINGS_1:def 3;
A58: not ax is empty

proof

assume ax is empty ; :: thesis:
then sa1 \ sa2 = {} by A57;
hence contradiction by A47, A49, A50, Thm26, Thm22; :: thesis:

end;

A59: sa1 \ sa2 <> {} by A49, A50, A47, Thm26, Thm22;
set x = { (product <*t*>) where t is Element of ax : verum } ;

now :: thesis:

deffunc H₁( object ) -> set = product <*$1*>;
consider f being Function such that
A60: dom f = ax and
A61: for x being object st x in ax holds
f . x = H₁(x) from FUNCT_1:sch 3();
rng f = { (product <*t*>) where t is Element of ax : verum }

proof

now :: thesis:

hereby :: thesis:

let t be object ; :: thesis:
assume t in rng f ; :: thesis:
then consider q being object such that
A62: q in dom f and
A63: t = f . q by FUNCT_1:def 3;
( t = product <*q*> & q in ax ) by A60, A61, A62, A63;
hence t in { (product <*t*>) where t is Element of ax : verum } ; :: thesis:

end;

let t be object ; :: thesis:
assume t in { (product <*t*>) where t is Element of ax : verum } ; :: thesis:
then consider u being Element of ax such that
A64: t = product <*u*> ;
f . u = H₁(u) by A61, A58;
hence t in rng f by A64, A60, A58, FUNCT_1:def 3; :: thesis:

end;

hence { (product <*t*>) where t is Element of ax : verum } is finite by A60, FINSET_1:8; :: thesis:
{ (product <*t*>) where t is Element of ax : verum } c= S2

proof

let t be object ; :: according to TARSKI:def 3 :: thesis:
assume t in { (product <*t*>) where t is Element of ax : verum } ; :: thesis:
then consider u being Element of ax such that
A65: t = product <*u*> ;
( u in ax & ax c= S . 1 ) by A58;
hence t in S2 by A65; :: thesis:

end;

hence { (product <*t*>) where t is Element of ax : verum } is Subset of S2 ; :: thesis:

now :: thesis:

A66: { (product <*t*>) where t is Element of ax : verum } c= bool (s1 \ s2)

proof

let t be object ; :: according to TARSKI:def 3 :: thesis:
assume t in { (product <*t*>) where t is Element of ax : verum } ; :: thesis:
then consider u0 being Element of ax such that
A67: t = product <*u0*> ;
reconsider t1 = t as set by A67;

per cases ;

suppose A68: t1 is empty ; :: thesis:

{} c= s1 \ s2 ;
hence t in bool (s1 \ s2) by A68; :: thesis:

end;

suppose A69: not t1 is empty ; :: thesis:

then A71: t = { <*y*> where y is Element of u0 : verum } by A67, Thm22, Thm23;
t1 c= s1 \ s2

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in t1 ; :: thesis:
then consider z being Element of u0 such that
A72: y = <*z*> by A71;
A73: product <*(sa1 \ sa2)*> = { <*a*> where a is Element of sa1 \ sa2 : verum } by A59, Thm23;
( u0 in ax & union ax = sa1 \ sa2 ) by A57, A58, EQREL_1:def 4;
then z in sa1 \ sa2 by A67, A69, Thm22, TARSKI:def 4;
then y in product <*(sa1 \ sa2)*> by A72, A73;
hence y in s1 \ s2 by A49, A50, Thm26; :: thesis:

end;

hence t in bool (s1 \ s2) ; :: thesis:

end;

hence { (product <*t*>) where t is Element of ax : verum } is Subset-Family of (s1 \ s2) ; :: thesis:

now :: thesis:

hereby :: thesis:

let a be object ; :: thesis:
assume a in union { (product <*t*>) where t is Element of ax : verum } ; :: thesis:
then consider b being set such that
A74: a in b and
A75: b in { (product <*t*>) where t is Element of ax : verum } by TARSKI:def 4;
thus a in s1 \ s2 by A66, A74, A75; :: thesis:

end;

let a be object ; :: thesis:
assume A76: a in s1 \ s2 ; :: thesis:
A77: a in product <*(sa1 \ sa2)*> by Thm26, A76, A49, A50;
product <*(sa1 \ sa2)*> = { <*u*> where u is Element of sa1 \ sa2 : verum } by A59, Thm23;
then consider b being Element of sa1 \ sa2 such that
A78: a = <*b*> by A77;
( b in sa1 \ sa2 & union ax = sa1 \ sa2 ) by A59, A57, EQREL_1:def 4;
then consider d being set such that
A79: ( b in d & d in ax ) by TARSKI:def 4;
A80: product <*d*> = { <*u*> where u is Element of d : verum } by Thm23, A79;
( <*b*> in product <*d*> & product <*d*> in { (product <*t*>) where t is Element of ax : verum } ) by A79, A80;
hence a in union { (product <*t*>) where t is Element of ax : verum } by A78, TARSKI:def 4; :: thesis:

end;

then ( union { (product <*t*>) where t is Element of ax : verum } c= s1 \ s2 & s1 \ s2 c= union { (product <*t*>) where t is Element of ax : verum } ) ;
hence union { (product <*t*>) where t is Element of ax : verum } = s1 \ s2 ; :: thesis:

hereby :: thesis:

let A be Subset of (s1 \ s2); :: thesis:
assume A in { (product <*t*>) where t is Element of ax : verum } ; :: thesis:
then consider a being Element of ax such that
A81: A = product <*a*> ;
A82: a in ax by A58;
A83: A = { <*u*> where u is Element of a : verum } by A57, A58, A81, Thm23;
consider b being object such that
A84: b in a by A57, A58, XBOOLE_0:def 1;
<*b*> in A by A83, A84;
hence A <> {} ; :: thesis:
let B be Subset of (s1 \ s2); :: thesis:
assume B in { (product <*t*>) where t is Element of ax : verum } ; :: thesis:
then consider b being Element of ax such that
A85: B = product <*b*> ;
A86: b in ax by A58;
( a misses b implies A misses B ) by A81, A85, Thm25, Thm22;
hence ( A = B or A misses B ) by A86, A81, A85, A82, A57, EQREL_1:def 4; :: thesis:

end;

hence { (product <*t*>) where t is Element of ax : verum } is a_partition of s1 \ s2 by EQREL_1:def 4; :: thesis:

end;

hence ex x being finite Subset of S2 st x is a_partition of s1 \ s2 ; :: thesis:

end;

hence S2 is diff-c=-finite-partition-closed ; :: thesis:

end;

hence { (product <*s*>) where s is Element of S . 1 : verum } is semiring_of_sets of { <*x*> where x is Element of X . 1 : verum } ; :: thesis:

end;

hence { (product <*s*>) where s is Element of S . 1 : verum } is semiring_of_sets of { <*x*> where x is Element of X . 1 : verum } ; :: thesis: