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 A3, FUNCT_1:def 3;
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 S₁[ object , object ] means ( $2 = x & $2 in F . $1 );
A6: {i} c= J by A4, ZFMISC_1:31;
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 & S₁[j,y] )

proof

let j be object ; :: thesis: ( j in E implies ex y being object st
( y in Sigma & S₁[j,y] ) )
assume A8: j in E ; :: thesis: ex y being object st
( y in Sigma & S₁[j,y] )
i in I by A4, TARSKI:def 3;
then A9: F . i in bool Sigma by FUNCT_2:5;
take y = x; :: thesis: ( y in Sigma & S₁[j,y] )
y in F . i by A2, A4, A5, FUNCT_1:49;
hence ( y in Sigma & S₁[j,y] ) by A8, A9, TARSKI:def 1; :: thesis: verum

end;

consider g being Function of E,Sigma such that
A10: for j being object st j in E holds
S₁[j,g . j] from FUNCT_2:sch 1(A7);
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 A11, SETFAM_1:10 ;
hence x in MeetSections (J,F) by A6, Def9; :: 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 S₁[ 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 S₁[B9] & not b in B9 holds
S₁[B9 \/ {b}]

proof

let B9 be Element of Fin E; :: thesis: for b being Element of E st S₁[B9] & not b in B9 holds
S₁[B9 \/ {b}]
let b be Element of E; :: thesis: ( S₁[B9] & not b in B9 implies S₁[B9 \/ {b}] )
assume that
A15: meet (rng (f | B9)) in sigma (Union (F | J)) and
not b in B9 ; :: thesis: S₁[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 A17, FUNCT_1:47;
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 A20, FUNCT_1:4
.= {(f . b)} by A21, FUNCT_1:47 ;
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: S₁[B9 \/ {b}]

hence S₁[B9 \/ {b}] by A22, A19, A16; :: thesis: verum

end;

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

( dom f = E & b in {b} ) by FUNCT_2:def 1, TARSKI:def 1;
then rfb <> {} by FUNCT_1:50;
then meet rfB9b = (meet rfB9) /\ (meet rfb) by A16, A23, SETFAM_1:9;
then meet (rng (f | (B9 \/ {b}))) is Event of sigma (Union (F | J)) by A15, A22, A19, PROB_1:19;
hence S₁[B9 \/ {b}] ; :: thesis: verum

end;

end;

end;

meet (rng (f | {})) = {} by SETFAM_1:def 1;
then A24: S₁[ {}. E] by PROB_1:4;
for B1 being Element of Fin E holds S₁[B1] from SETWISEO:sch 2(A24, A14);
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