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)

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

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

MeetSections (J,F) c= sigma (Union (F | J))
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_{1}[ 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_{1}[j,y] )

A10: for j being object st j in E holds

S_{1}[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;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

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

proof

consider g being Function of E,Sigma such that
let j be object ; :: thesis: ( j in E implies ex y being object st

( y in Sigma & S_{1}[j,y] ) )

assume A8: j in E ; :: thesis: ex y being object st

( y in Sigma & S_{1}[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_{1}[j,y] )

y in F . i by A2, A4, A5, FUNCT_1:49;

hence ( y in Sigma & S_{1}[j,y] )
by A8, A9, TARSKI:def 1; :: thesis: verum

end;( y in Sigma & S

assume A8: j in E ; :: thesis: ex y being object st

( y in Sigma & S

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

y in F . i by A2, A4, A5, FUNCT_1:49;

hence ( y in Sigma & S

A10: for j being object st j in E holds

S

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

proof

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))
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))

hence x in sigma (Union (F | J)) by A13; :: thesis: verum

end;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

then
meet (rng (f | Ee)) in sigma (Union (F | J))
;
defpred S_{1}[ 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_{1}[B9] & not b in B9 holds

S_{1}[B9 \/ {b}]

then A24: S_{1}[ {}. E]
by PROB_1:4;

for B1 being Element of Fin E holds S_{1}[B1]
from SETWISEO:sch 2(A24, A14);

hence meet (rng (f | B)) in sigma (Union (F | J)) ; :: thesis: verum

end;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

S

proof

meet (rng (f | {})) = {}
by SETFAM_1:def 1;
let B9 be Element of Fin E; :: thesis: for b being Element of E st S_{1}[B9] & not b in B9 holds

S_{1}[B9 \/ {b}]

let b be Element of E; :: thesis: ( S_{1}[B9] & not b in B9 implies S_{1}[B9 \/ {b}] )

assume that

A15: meet (rng (f | B9)) in sigma (Union (F | J)) and

not b in B9 ; :: thesis: S_{1}[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;

end;S

let b be Element of E; :: thesis: ( S

assume that

A15: meet (rng (f | B9)) in sigma (Union (F | J)) and

not b in B9 ; :: thesis: S

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) = {} )
;

end;

suppose A23:
not rng (f | B9) = {}
; :: thesis: S_{1}[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_{1}[B9 \/ {b}]
; :: thesis: verum

end;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

then A24: S

for B1 being Element of Fin E holds S

hence meet (rng (f | B)) in sigma (Union (F | J)) ; :: thesis: verum

hence x in sigma (Union (F | J)) by A13; :: thesis: verum

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