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)
A1: Union (F | J) c= MeetSections (J,F)
proof
let x be object ; :: 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
A2: x in y and
A3: y in rng (F | J) by TARSKI:def 4;
consider i being object such that
A4: i in dom (F | J) and
A5: y = (F | J) . i by ;
reconsider i = i as set by TARSKI:1;
y = (F | J) . i by A5;
then reconsider x = x as Subset of Omega by A2;
defpred S1[ object , object ] means ( \$2 = x & \$2 in F . \$1 );
A6: {i} c= J by ;
then reconsider E = {i} as finite Subset of I by XBOOLE_1:1;
A7: for j being object st j in E holds
ex y being object st
( y in Sigma & S1[j,y] )
proof
let j be object ; :: thesis: ( j in E implies ex y being object st
( y in Sigma & S1[j,y] ) )

assume A8: j in E ; :: thesis: ex y being object st
( y in Sigma & S1[j,y] )

i in I by ;
then A9: F . i in bool Sigma by FUNCT_2:5;
take y = x; :: thesis: ( y in Sigma & S1[j,y] )
y in F . i by ;
hence ( y in Sigma & S1[j,y] ) by ; :: thesis: verum
end;
consider g being Function of E,Sigma such that
A10: for j being object st j in E holds
S1[j,g . j] from for i being set st i in E holds
g . i in F . i by A10;
then reconsider g = g as SigmaSection of E,F by Def4;
dom g = E by FUNCT_2:def 1;
then A11: rng g = {(g . i)} by FUNCT_1:4;
i in E by TARSKI:def 1;
then x = g . i by A10
.= meet (rng g) by ;
hence x in MeetSections (J,F) by ; :: thesis: verum
end;
MeetSections (J,F) c= sigma (Union (F | J))
proof
let x be object ; :: 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
A12: E c= J and
A13: x = meet (rng f) by Def9;
reconsider Ee = E as Element of Fin E by FINSUB_1:def 5;
for B being Element of Fin E holds meet (rng (f | B)) in sigma (Union (F | J))
proof
defpred S1[ set ] means meet (rng (f | \$1)) in sigma (Union (F | J));
let B be Element of Fin E; :: thesis: meet (rng (f | B)) in sigma (Union (F | J))
A14: for B9 being Element of Fin E
for b being Element of E st S1[B9] & not b in B9 holds
S1[B9 \/ {b}]
proof
let B9 be Element of Fin E; :: thesis: for b being Element of E st S1[B9] & not b in B9 holds
S1[B9 \/ {b}]

let b be Element of E; :: thesis: ( S1[B9] & not b in B9 implies S1[B9 \/ {b}] )
assume that
A15: meet (rng (f | B9)) in sigma (Union (F | J)) and
not b in B9 ; :: thesis: S1[B9 \/ {b}]
reconsider rfb = rng (f | {b}) as set ;
reconsider rfB9 = rng (f | B9) as set ;
reconsider rfB9b = rng (f | (B9 \/ {b})) as set ;
rng (f | (B9 \/ {b})) = rng ((f | B9) \/ (f | {b})) by RELAT_1:78;
then A16: rng (f | (B9 \/ {b})) = (rng (f | B9)) \/ (rng (f | {b})) by RELAT_1:12;
dom (F | J) = J by FUNCT_2:def 1;
then A17: b in dom (F | J) by A12;
then (F | J) . b in rng (F | J) by FUNCT_1:def 3;
then F . b in rng (F | J) by ;
then A18: F . b c= Union (F | J) by ZFMISC_1:74;
Union (F | J) c= sigma (Union (F | J)) by PROB_1:def 9;
then A19: F . b c= sigma (Union (F | J)) by A18;
b is Element of dom f by FUNCT_2:def 1;
then A20: {b} = (dom f) /\ {b} by ZFMISC_1:46
.= dom (f | {b}) by RELAT_1:61 ;
then A21: b in dom (f | {b}) by TARSKI:def 1;
rng (f | {b}) = {((f | {b}) . b)} by
.= {(f . b)} by ;
then meet (rng (f | {b})) = f . b by SETFAM_1:10;
then A22: meet (rng (f | {b})) in F . b by Def4;
per cases ( rng (f | B9) = {} or not rng (f | B9) = {} ) ;
suppose rng (f | B9) = {} ; :: thesis: S1[B9 \/ {b}]
hence S1[B9 \/ {b}] by ; :: thesis: verum
end;
suppose A23: not rng (f | B9) = {} ; :: thesis: S1[B9 \/ {b}]
( dom f = E & b in {b} ) by ;
then rfb <> {} by FUNCT_1:50;
then meet rfB9b = (meet rfB9) /\ (meet rfb) by ;
then meet (rng (f | (B9 \/ {b}))) is Event of sigma (Union (F | J)) by ;
hence S1[B9 \/ {b}] ; :: thesis: verum
end;
end;
end;
meet (rng (f | {})) = {} by SETFAM_1:def 1;
then A24: S1[ {}. E] by PROB_1:4;
for B1 being Element of Fin E holds S1[B1] from hence meet (rng (f | B)) in sigma (Union (F | J)) ; :: thesis: verum
end;
then meet (rng (f | Ee)) in sigma (Union (F | J)) ;
hence x in sigma (Union (F | J)) by A13; :: thesis: verum
end;
hence sigma (MeetSections (J,F)) c= sigUn (F,J) by PROB_1:def 9; :: according to XBOOLE_0:def 10 :: thesis: sigUn (F,J) c= sigma (MeetSections (J,F))
MeetSections (J,F) c= sigma (MeetSections (J,F)) by PROB_1:def 9;
then Union (F | J) c= sigma (MeetSections (J,F)) by A1;
hence sigUn (F,J) c= sigma (MeetSections (J,F)) by PROB_1:def 9; :: thesis: verum