let Omega, I be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for F being ManySortedSigmaField of I,Sigma
for J being non empty Subset of I holds sigma (MeetSections J,F) = sigUn F,J
let Sigma be SigmaField of Omega; :: thesis: for F being ManySortedSigmaField of I,Sigma
for J being non empty Subset of I holds sigma (MeetSections J,F) = sigUn F,J
let F be ManySortedSigmaField of I,Sigma; :: thesis: for J being non empty Subset of I holds sigma (MeetSections J,F) = sigUn F,J
let J be non empty Subset of I; :: thesis: sigma (MeetSections J,F) = sigUn F,J
thus sigma (MeetSections J,F) c= sigUn F,J :: according to XBOOLE_0:def 10 :: thesis: sigUn F,J c= sigma (MeetSections J,F)

proof

MeetSections J,F c= sigma (Union (F | J))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in MeetSections J,F or x in sigma (Union (F | J)) )
assume x in MeetSections J,F ; :: thesis: x in sigma (Union (F | J))
then consider E being non empty finite Subset of I, f being SigmaSection of E,F such that
D0: ( E c= J & x = meet (rng f) ) by Def9;
D1: for B being Element of Fin E holds meet (rng (f | B)) in sigma (Union (F | J))

proof

let B be Element of Fin E; :: thesis: meet (rng (f | B)) in sigma (Union (F | J))
defpred S₁[ set ] means meet (rng (f | $1)) in sigma (Union (F | J));
meet (rng (f | {} )) = {} by SETFAM_1:def 1;
then E0: S₁[ {}. E] by PROB_1:42;
E1: for B' being Element of Fin E
for b being Element of E st S₁[B'] & not b in B' holds
S₁[B' \/ {b}]

proof

let B' be Element of Fin E; :: thesis: for b being Element of E st S₁[B'] & not b in B' holds
S₁[B' \/ {b}]
let b be Element of E; :: thesis: ( S₁[B'] & not b in B' implies S₁[B' \/ {b}] )
assume Z: ( meet (rng (f | B')) in sigma (Union (F | J)) & not b in B' ) ; :: thesis: S₁[B' \/ {b}]
F1: meet (rng (f | {b})) is Event of sigma (Union (F | J))

proof

b is Element of dom f by FUNCT_2:def 1;
then G0: {b} = (dom f) /\ {b} by ZFMISC_1:52
.= dom (f | {b}) by RELAT_1:90 ;
then G1: b in dom (f | {b}) by TARSKI:def 1;
rng (f | {b}) = {((f | {b}) . b)} by G0, FUNCT_1:14
.= {(f . b)} by G1, FUNCT_1:70 ;
then meet (rng (f | {b})) = f . b by SETFAM_1:11;
then G2: meet (rng (f | {b})) in F . b by Def4;
dom (F | J) = J by FUNCT_2:def 1;
then G3: b in dom (F | J) by D0, TARSKI:def 3;
then (F | J) . b in rng (F | J) by FUNCT_1:def 5;
then F . b in rng (F | J) by G3, FUNCT_1:70;
then ( F . b c= Union (F | J) & Union (F | J) c= sigma (Union (F | J)) ) by PROB_1:def 14, ZFMISC_1:92;
then F . b c= sigma (Union (F | J)) by XBOOLE_1:1;
hence meet (rng (f | {b})) is Event of sigma (Union (F | J)) by G2; :: thesis: verum

end;

rng (f | (B' \/ {b})) = rng ((f | B') \/ (f | {b})) by RELAT_1:107;
then F2: rng (f | (B' \/ {b})) = (rng (f | B')) \/ (rng (f | {b})) by RELAT_1:26;
reconsider rfB'b = rng (f | (B' \/ {b})) as set ;
reconsider rfB' = rng (f | B') as set ;
reconsider rfb = rng (f | {b}) as set ;

per cases ( rng (f | B') = {} or not rng (f | B') = {} ) ;

suppose rng (f | B') = {} ; :: thesis: S₁[B' \/ {b}]

hence S₁[B' \/ {b}] by F1, F2; :: thesis: verum

end;

suppose G1: not rng (f | B') = {} ; :: thesis: S₁[B' \/ {b}]

dom f = E by FUNCT_2:def 1;
then ( b in dom f & b in {b} ) by TARSKI:def 1;
then ( rfB' <> {} & rfb <> {} ) by G1, FUNCT_1:73;
then meet rfB'b = (meet rfB') /\ (meet rfb) by F2, SETFAM_1:10;
then meet (rng (f | (B' \/ {b}))) is Event of sigma (Union (F | J)) by Z, F1, PROB_1:49;
hence S₁[B' \/ {b}] ; :: thesis: verum

end;

end;

end;

for B1 being Element of Fin E holds S₁[B1] from SETWISEO:sch 2(E0, E1);
hence meet (rng (f | B)) in sigma (Union (F | J)) ; :: thesis: verum

end;

reconsider Ee = E as Element of Fin E by FINSUB_1:def 5;
meet (rng (f | Ee)) in sigma (Union (F | J)) by D1;
hence x in sigma (Union (F | J)) by D0, RELSET_1:34; :: thesis: verum

end;

hence sigma (MeetSections J,F) c= sigUn F,J by PROB_1:def 14; :: thesis: verum

end;

B0: Union (F | J) c= MeetSections J,F

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Union (F | J) or x in MeetSections J,F )
assume x in Union (F | J) ; :: thesis: x in MeetSections J,F
then consider y being set such that
D0: ( x in y & y in rng (F | J) ) by TARSKI:def 4;
consider i being set such that
D1: ( i in dom (F | J) & y = (F | J) . i ) by D0, FUNCT_1:def 5;
reconsider x = x as Subset of Omega by D0, D1;
D2: {i} c= J by D1, ZFMISC_1:37;
then reconsider E = {i} as finite Subset of I by XBOOLE_1:1;
defpred S₁[ set , set ] means ( $2 = x & $2 in F . $1 );
D4: for j being set st j in E holds
ex y being set st
( y in Sigma & S₁[j,y] )

proof

let j be set ; :: thesis: ( j in E implies ex y being set st
( y in Sigma & S₁[j,y] ) )
assume E0: j in E ; :: thesis: ex y being set st
( y in Sigma & S₁[j,y] )
take y = x; :: thesis: ( y in Sigma & S₁[j,y] )
( Sigma <> {} & i in I ) by D1, TARSKI:def 3;
then X: F . i in bool Sigma by FUNCT_2:7;
y in F . i by D0, D1, FUNCT_1:72;
hence ( y in Sigma & S₁[j,y] ) by E0, X, TARSKI:def 1; :: thesis: verum

end;

consider g being Function of E,Sigma such that
D5: for j being set st j in E holds
S₁[j,g . j] from FUNCT_2:sch 1(D4);
for i being set st i in E holds
g . i in F . i by D5;
then reconsider g = g as SigmaSection of E,F by Def4;
dom g = E by FUNCT_2:def 1;
then D7: rng g = {(g . i)} by FUNCT_1:14;
i in E by TARSKI:def 1;
then x = g . i by D5
.= meet (rng g) by D7, SETFAM_1:11 ;
hence x in MeetSections J,F by D2, Def9; :: thesis: verum

end;

MeetSections J,F c= sigma (MeetSections J,F) by PROB_1:def 14;
then Union (F | J) c= sigma (MeetSections J,F) by B0, XBOOLE_1:1;
hence sigUn F,J c= sigma (MeetSections J,F) by PROB_1:def 14; :: thesis: verum