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 MeetSections J,F is non empty Subset of Sigma
let Sigma be SigmaField of Omega; :: thesis: for F being ManySortedSigmaField of I,Sigma
for J being non empty Subset of I holds MeetSections J,F is non empty Subset of Sigma
let F be ManySortedSigmaField of I,Sigma; :: thesis: for J being non empty Subset of I holds MeetSections J,F is non empty Subset of Sigma
let J be non empty Subset of I; :: thesis: MeetSections J,F is non empty Subset of Sigma
A0: MeetSections J,F is non empty set

proof

consider E being non empty finite Subset of J;
consider f being Function such that
B0: ( dom f = E & rng f = {{} } ) by FUNCT_1:15;
B1: meet (rng f) = {} by B0, SETFAM_1:11;
B2: rng f c= Sigma

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in Sigma )
assume y in rng f ; :: thesis: y in Sigma
then y = {} by B0, TARSKI:def 1;
hence y in Sigma by PROB_1:10; :: thesis: verum

end;

reconsider E = E as non empty finite Subset of I by XBOOLE_1:1;
reconsider f = f as Function of E,Sigma by B0, B2, FUNCT_2:4;
for i being set st i in E holds
f . i in F . i

proof

let i be set ; :: thesis: ( i in E implies f . i in F . i )
assume C0: i in E ; :: thesis: f . i in F . i
then f . i in rng f by B0, FUNCT_1:def 5;
then C1: f . i = {} by B0, TARSKI:def 1;
reconsider Fi = F . i as SigmaField of Omega by C0, Def2;
f . i in Fi by C1, PROB_1:10;
hence f . i in F . i ; :: thesis: verum

end;

then reconsider f = f as SigmaSection of E,F by Def4;
reconsider mrf = meet (rng f) as Subset of Omega by B1, XBOOLE_1:2;
mrf in MeetSections J,F by Def9;
hence MeetSections J,F is non empty set ; :: thesis: verum

end;

MeetSections J,F c= Sigma

proof

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

proof

let B be Element of Fin E; :: thesis: meet (rng (f | B)) in Sigma
defpred S₁[ set ] means meet (rng (f | $1)) in Sigma;
D0: S₁[ {}. E]

proof

meet (rng (f | {} )) = {} by SETFAM_1:def 1;
hence S₁[ {}. E] by PROB_1:42; :: thesis: verum

end;

D1: 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 & not b in B' ) ; :: thesis: S₁[B' \/ {b}]
E1: meet (rng (f | {b})) is Event of Sigma

proof

F0: b is Element of dom f by FUNCT_2:def 1;
then (dom f) /\ {b} = {b} by ZFMISC_1:52;
then dom (f | {b}) = {b} by RELAT_1:90;
then F1: rng (f | {b}) = {((f | {b}) . b)} by FUNCT_1:14;
( b in {b} & b in dom f ) by F0, TARSKI:def 1;
then b in dom (f | {b}) by RELAT_1:86;
then rng (f | {b}) = {(f . b)} by F1, FUNCT_1:70;
hence meet (rng (f | {b})) is Event of Sigma by SETFAM_1:11; :: thesis: verum

end;

E2: rng (f | (B' \/ {b})) = rng ((f | B') \/ (f | {b})) by RELAT_1:107
.= (rng (f | B')) \/ (rng (f | {b})) by RELAT_1:26 ;
E3: dom f = E by FUNCT_2:def 1;
reconsider domf = dom f as non empty set ;
( b in domf & b in {b} ) by E3, TARSKI:def 1;
then E4: f . b in rng (f | {b}) by FUNCT_1:73;

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

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

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

end;

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

then meet (rng (f | (B' \/ {b}))) = (meet (rng (f | B'))) /\ (meet (rng (f | {b}))) by E2, E4, SETFAM_1:10;
then meet (rng (f | (B' \/ {b}))) is Event of Sigma by Z, E1, 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(D0, D1);
hence meet (rng (f | B)) in Sigma ; :: thesis: verum

end;

reconsider Ee = E as Element of Fin E by FINSUB_1:def 5;
meet (rng (f | Ee)) in Sigma by C1;
hence X in Sigma by C0, RELSET_1:34; :: thesis: verum

end;

hence MeetSections J,F is non empty Subset of Sigma by A0; :: thesis: verum