for x, X being set st x in MeetSections J,F & X in MeetSections J,F holds
x /\ X in MeetSections J,F

proof

let x, X be set ; :: thesis: ( x in MeetSections J,F & X in MeetSections J,F implies x /\ X in MeetSections J,F )
assume that
A1: x in MeetSections J,F and
A2: X in MeetSections J,F ; :: thesis: x /\ X in MeetSections J,F
consider E being non empty finite Subset of , f being SigmaSection of E,F such that
A3: E c= J and
A4: x = meet (rng f) by A1, Def9;
defpred S₁[ set ] means I in E;
deffunc H₁( set ) -> set = f . I;
consider E' being non empty finite Subset of , f' being SigmaSection of E',F such that
A5: E' c= J and
A6: X = meet (rng f') by A2, Def9;
deffunc H₂( set ) -> set = f' . I;
defpred S₂[ set ] means I in (E \ E') \/ (E' \ E);
deffunc H₃( set ) -> set = (f . I) /\ (f' . I);
consider h being Function such that
A7: ( dom h = E \/ E' & ( for i being set st i in E \/ E' holds
( ( S₁[i] implies h . i = H₁(i) ) & ( not S₁[i] implies h . i = H₂(i) ) ) ) ) from PARTFUN1:sch 1();
deffunc H₄( set ) -> set = h . I;
consider g being Function such that
A8: ( dom g = E \/ E' & ( for i being set st i in E \/ E' holds
( ( S₂[i] implies g . i = H₄(i) ) & ( not S₂[i] implies g . i = H₃(i) ) ) ) ) from PARTFUN1:sch 1();
A9: for i being set st i in E \/ E' holds
g . i in F . i

proof

let i be set ; :: thesis: ( i in E \/ E' implies g . i in F . i )
assume A10: i in E \/ E' ; :: thesis: g . i in F . i

per cases ( i in (E \ E') \/ (E' \ E) or not i in (E \ E') \/ (E' \ E) ) ;

suppose A11: i in (E \ E') \/ (E' \ E) ; :: thesis: g . i in F . i

h . i in F . i

proof

per cases ( i in E or not i in E ) ;

suppose A12: i in E ; :: thesis: h . i in F . i

then h . i = f . i by A7, A10;
hence h . i in F . i by A12, Def4; :: thesis: verum

end;

suppose not i in E ; :: thesis: h . i in F . i

then ( i in E' & h . i = f' . i ) by A7, A10, XBOOLE_0:def 3;
hence h . i in F . i by Def4; :: thesis: verum

end;

end;

end;

hence g . i in F . i by A8, A10, A11; :: thesis: verum

end;

suppose A13: not i in (E \ E') \/ (E' \ E) ; :: thesis: g . i in F . i

reconsider Fi = F . i as SigmaField of Omega by A10, Def2;
not i in E \+\ E' by A13;
then ( i in E iff i in E' ) by XBOOLE_0:1;
then ( f . i in F . i & f' . i in F . i ) by A10, Def4, XBOOLE_0:def 3;
then A14: (f . i) /\ (f' . i) is Event of Fi by PROB_1:49;
g . i = (f . i) /\ (f' . i) by A8, A10, A13;
hence g . i in F . i by A14; :: thesis: verum

end;

end;

end;

rng g c= Sigma

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng g or y in Sigma )
assume y in rng g ; :: thesis: y in Sigma
then consider i being set such that
A15: ( i in dom g & y = g . i ) by FUNCT_1:def 5;
( y in F . i & F . i in bool Sigma ) by A8, A9, A15, FUNCT_2:7;
hence y in Sigma ; :: thesis: verum

end;

then g is Function of E \/ E',Sigma by A8, FUNCT_2:4;
then reconsider g = g as SigmaSection of E \/ E',F by A9, Def4;
A16: x /\ X = meet (rng g)

proof

A17: meet (rng (g | (E /\ E'))) = (meet (rng (f | (E /\ E')))) /\ (meet (rng (f' | (E /\ E'))))

proof

per cases ( E /\ E' = {} or not E /\ E' = {} ) ;

suppose A18: E /\ E' = {} ; :: thesis: meet (rng (g | (E /\ E'))) = (meet (rng (f | (E /\ E')))) /\ (meet (rng (f' | (E /\ E'))))

then A19: ( meet (rng (f | (E /\ E'))) = meet (rng {} ) & meet (rng (f' | (E /\ E'))) = meet (rng {} ) ) ;
meet (rng (g | (E /\ E'))) = meet (rng {} ) by A18
.= {} by SETFAM_1:def 1 ;
hence meet (rng (g | (E /\ E'))) = (meet (rng (f | (E /\ E')))) /\ (meet (rng (f' | (E /\ E')))) by A19, SETFAM_1:def 1; :: thesis: verum

end;

suppose not E /\ E' = {} ; :: thesis: meet (rng (g | (E /\ E'))) = (meet (rng (f | (E /\ E')))) /\ (meet (rng (f' | (E /\ E'))))

then reconsider EnE' = E /\ E' as non empty set ;
reconsider EE' = EnE' as Element of Fin EnE' by FINSUB_1:def 5;
for B being Element of Fin EnE' holds meet (rng (g | B)) = (meet (rng (f | B))) /\ (meet (rng (f' | B)))

proof

defpred S₃[ set ] means meet (rng (g | I)) = (meet (rng (f | I))) /\ (meet (rng (f' | I)));
let B be Element of Fin EnE'; :: thesis: meet (rng (g | B)) = (meet (rng (f | B))) /\ (meet (rng (f' | B)))
A20: for B' being Element of Fin EnE'
for b being Element of EnE' st S₃[B'] & not b in B' holds
S₃[B' \/ {b}]

proof

let B' be Element of Fin EnE'; :: thesis: for b being Element of EnE' st S₃[B'] & not b in B' holds
S₃[B' \/ {b}]
let b be Element of EnE'; :: thesis: ( S₃[B'] & not b in B' implies S₃[B' \/ {b}] )
assume that
A21: meet (rng (g | B')) = (meet (rng (f | B'))) /\ (meet (rng (f' | B'))) and
not b in B' ; :: thesis: S₃[B' \/ {b}]
A22: dom (f | {b}) = (dom f) /\ {b} by RELAT_1:90;
dom f = E by FUNCT_2:def 1;
then A23: E /\ E' c= dom f by XBOOLE_1:17;
then b in dom f by TARSKI:def 3;
then A24: rng (f | {b}) = {((f | {b}) . b)} by A22, FUNCT_1:14, ZFMISC_1:52;
b in (E \ (E \/ E')) \/ ((E /\ E) /\ E') by XBOOLE_0:def 3;
then b in E \ (E \+\ E') by XBOOLE_1:102;
then A25: not b in E \+\ E' by XBOOLE_0:def 5;
A26: b in {b} by TARSKI:def 1;
b in dom f by A23, TARSKI:def 3;
then b in dom (f | {b}) by A26, RELAT_1:86;
then A27: rng (f | {b}) = {(f . b)} by A24, FUNCT_1:70;
then A28: meet (rng (f | {b})) = f . b by SETFAM_1:11;
A29: E /\ E' c= E by XBOOLE_1:17;
A30: dom (f' | {b}) = (dom f') /\ {b} by RELAT_1:90;
dom f' = E' by FUNCT_2:def 1;
then A31: E /\ E' c= dom f' by XBOOLE_1:17;
then b in dom f' by TARSKI:def 3;
then A32: rng (f' | {b}) = {((f' | {b}) . b)} by A30, FUNCT_1:14, ZFMISC_1:52;
b in dom f' by A31, TARSKI:def 3;
then b in dom (f' | {b}) by A26, RELAT_1:86;
then A33: rng (f' | {b}) = {(f' . b)} by A32, FUNCT_1:70;
then A34: meet (rng (f' | {b})) = f' . b by SETFAM_1:11;
A35: for g being Function
for B', b being set holds meet (rng (g | (B' \/ {b}))) = meet ((rng (g | B')) \/ (rng (g | {b})))

proof

let g be Function; :: thesis: for B', b being set holds meet (rng (g | (B' \/ {b}))) = meet ((rng (g | B')) \/ (rng (g | {b})))
let B', b be set ; :: thesis: meet (rng (g | (B' \/ {b}))) = meet ((rng (g | B')) \/ (rng (g | {b})))
rng (g | (B' \/ {b})) = rng ((g | B') \/ (g | {b})) by RELAT_1:107;
hence meet (rng (g | (B' \/ {b}))) = meet ((rng (g | B')) \/ (rng (g | {b}))) by RELAT_1:26; :: thesis: verum

end;

E c= dom g by A8, XBOOLE_1:7;
then A36: E /\ E' c= dom g by A29, XBOOLE_1:1;
then b is Element of dom g by TARSKI:def 3;
then (dom g) /\ {b} = {b} by ZFMISC_1:52;
then dom (g | {b}) = {b} by RELAT_1:90;
then A37: rng (g | {b}) = {((g | {b}) . b)} by FUNCT_1:14;
( b in {b} & b in dom g ) by A36, TARSKI:def 1, TARSKI:def 3;
then b in dom (g | {b}) by RELAT_1:86;
then A38: rng (g | {b}) = {(g . b)} by A37, FUNCT_1:70;
then A39: meet (rng (g | {b})) = g . b by SETFAM_1:11;
E c= E \/ E' by XBOOLE_1:7;
then A40: E /\ E' c= E \/ E' by A29, XBOOLE_1:1;
then b in E \/ E' by TARSKI:def 3;
then A41: g . b = (f . b) /\ (f' . b) by A8, A25;

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

suppose B' = {} ; :: thesis: S₃[B' \/ {b}]

hence S₃[B' \/ {b}] by A28, A34, A41, A38, SETFAM_1:11; :: thesis: verum

end;

suppose A42: not B' = {} ; :: thesis: S₃[B' \/ {b}]

consider z being Element of B';
B' c= E /\ E' by FINSUB_1:def 5;
then A43: B' c= E \/ E' by A40, XBOOLE_1:1;
z in B' by A42;
then z in dom (g | B') by A8, A43, RELAT_1:86;
then ex y being set st y in rng (g | B') by RELAT_1:18;
then meet ((rng (g | B')) \/ (rng (g | {b}))) = (meet (rng (g | B'))) /\ (meet (rng (g | {b}))) by A37, SETFAM_1:10;
then A44: meet (rng (g | (B' \/ {b}))) = ((meet (rng (f | B'))) /\ (meet (rng (f' | B')))) /\ (g . b) by A21, A35, A39
.= (meet (rng (f | B'))) /\ ((meet (rng (f' | B'))) /\ ((f . b) /\ (f' . b))) by A41, XBOOLE_1:16
.= (meet (rng (f | B'))) /\ ((f . b) /\ ((meet (rng (f' | B'))) /\ (f' . b))) by XBOOLE_1:16
.= ((meet (rng (f | B'))) /\ (f . b)) /\ ((meet (rng (f' | B'))) /\ (f' . b)) by XBOOLE_1:16 ;
( B' c= E /\ E' & E /\ E' c= E' ) by FINSUB_1:def 5, XBOOLE_1:17;
then B' c= E' by XBOOLE_1:1;
then A45: B' c= dom f' by FUNCT_2:def 1;
( B' c= E /\ E' & E /\ E' c= E ) by FINSUB_1:def 5, XBOOLE_1:17;
then B' c= E by XBOOLE_1:1;
then A46: B' c= dom f by FUNCT_2:def 1;
meet (rng (f | (B' \/ {b}))) = meet ((rng (f | B')) \/ (rng (f | {b}))) by A35
.= (meet (rng (f | B'))) /\ (meet (rng (f | {b}))) by A24, A42, A46, SETFAM_1:10 ;
then A47: (meet (rng (f | B'))) /\ (f . b) = meet (rng (f | (B' \/ {b}))) by A27, SETFAM_1:11;
meet (rng (f' | (B' \/ {b}))) = meet ((rng (f' | B')) \/ (rng (f' | {b}))) by A35
.= (meet (rng (f' | B'))) /\ (meet (rng (f' | {b}))) by A32, A42, A45, SETFAM_1:10 ;
hence S₃[B' \/ {b}] by A33, A44, A47, SETFAM_1:11; :: thesis: verum

end;

end;

end;

A48: S₃[ {}. EnE'] ;
for B1 being Element of Fin EnE' holds S₃[B1] from SETWISEO:sch 2(A48, A20);
hence meet (rng (g | B)) = (meet (rng (f | B))) /\ (meet (rng (f' | B))) ; :: thesis: verum

end;

then meet (rng (g | EE')) = (meet (rng (f | EE'))) /\ (meet (rng (f' | EE'))) ;
hence meet (rng (g | (E /\ E'))) = (meet (rng (f | (E /\ E')))) /\ (meet (rng (f' | (E /\ E')))) ; :: thesis: verum

end;

end;

end;

A49: for E, E' being set
for g being Function st dom g = E \/ E' holds
rng g = ((rng (g | (E /\ E'))) \/ (rng (g | (E \ E')))) \/ (rng (g | (E' \ E)))

proof

let E, E' be set ; :: thesis: for g being Function st dom g = E \/ E' holds
rng g = ((rng (g | (E /\ E'))) \/ (rng (g | (E \ E')))) \/ (rng (g | (E' \ E)))
let g be Function; :: thesis: ( dom g = E \/ E' implies rng g = ((rng (g | (E /\ E'))) \/ (rng (g | (E \ E')))) \/ (rng (g | (E' \ E))) )
( rng (g | (E /\ E')) c= rng g & rng (g | (E \ E')) c= rng g ) by RELAT_1:99;
then A50: (rng (g | (E /\ E'))) \/ (rng (g | (E \ E'))) c= rng g by XBOOLE_1:8;
assume A51: dom g = E \/ E' ; :: thesis: rng g = ((rng (g | (E /\ E'))) \/ (rng (g | (E \ E')))) \/ (rng (g | (E' \ E)))
thus rng g c= ((rng (g | (E /\ E'))) \/ (rng (g | (E \ E')))) \/ (rng (g | (E' \ E))) :: according to XBOOLE_0:def 10 :: thesis: ((rng (g | (E /\ E'))) \/ (rng (g | (E \ E')))) \/ (rng (g | (E' \ E))) c= rng g

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng g or y in ((rng (g | (E /\ E'))) \/ (rng (g | (E \ E')))) \/ (rng (g | (E' \ E))) )
assume y in rng g ; :: thesis: y in ((rng (g | (E /\ E'))) \/ (rng (g | (E \ E')))) \/ (rng (g | (E' \ E)))
then consider i being set such that
A52: i in dom g and
A53: y = g . i by FUNCT_1:def 5;

per cases ( i in (E \ E') \/ (E' \ E) or not i in (E \ E') \/ (E' \ E) ) ;

suppose A54: i in (E \ E') \/ (E' \ E) ; :: thesis: y in ((rng (g | (E /\ E'))) \/ (rng (g | (E \ E')))) \/ (rng (g | (E' \ E)))

y in ((rng (g | (E /\ E'))) \/ (rng (g | (E \ E')))) \/ (rng (g | (E' \ E)))

proof

per cases ( i in E or not i in E ) ;

suppose A55: i in E ; :: thesis: y in ((rng (g | (E /\ E'))) \/ (rng (g | (E \ E')))) \/ (rng (g | (E' \ E)))

A56: E /\ E' c= E by XBOOLE_1:17;
E /\ ((E \ E') \/ (E' \ E)) = (E /\ (E \ E')) \/ (E /\ (E' \ E)) by XBOOLE_1:23
.= (E \ E') \/ (E /\ (E' \ E)) by XBOOLE_1:28
.= (E \ E') \/ ((E /\ E') \ E) by XBOOLE_1:49
.= (E \ E') \/ {} by A56, XBOOLE_1:37 ;
then i in E \ E' by A54, A55, XBOOLE_0:def 4;
then i in (dom g) /\ (E \ E') by A52, XBOOLE_0:def 4;
then A57: i in dom (g | (E \ E')) by RELAT_1:90;
then (g | (E \ E')) . i = y by A53, FUNCT_1:70;
then y in rng (g | (E \ E')) by A57, FUNCT_1:def 5;
then y in (rng (g | (E /\ E'))) \/ (rng (g | (E \ E'))) by XBOOLE_0:def 3;
hence y in ((rng (g | (E /\ E'))) \/ (rng (g | (E \ E')))) \/ (rng (g | (E' \ E))) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose A58: not i in E ; :: thesis: y in ((rng (g | (E /\ E'))) \/ (rng (g | (E \ E')))) \/ (rng (g | (E' \ E)))

((E \ E') \/ (E' \ E)) \ E = ((E \ E') \ E) \/ ((E' \ E) \ E) by XBOOLE_1:42
.= {} \/ ((E' \ E) \ E) by XBOOLE_1:37
.= E' \ (E \/ E) by XBOOLE_1:41 ;
then i in E' \ (E \/ E) by A54, A58, XBOOLE_0:def 5;
then i in (dom g) /\ (E' \ E) by A52, XBOOLE_0:def 4;
then A59: i in dom (g | (E' \ E)) by RELAT_1:90;
then (g | (E' \ E)) . i = y by A53, FUNCT_1:70;
then y in rng (g | (E' \ E)) by A59, FUNCT_1:def 5;
then y in (rng (g | (E \ E'))) \/ (rng (g | (E' \ E))) by XBOOLE_0:def 3;
then y in (rng (g | (E /\ E'))) \/ ((rng (g | (E \ E'))) \/ (rng (g | (E' \ E)))) by XBOOLE_0:def 3;
hence y in ((rng (g | (E /\ E'))) \/ (rng (g | (E \ E')))) \/ (rng (g | (E' \ E))) by XBOOLE_1:4; :: thesis: verum

end;

end;

end;

hence y in ((rng (g | (E /\ E'))) \/ (rng (g | (E \ E')))) \/ (rng (g | (E' \ E))) ; :: thesis: verum

end;

suppose A60: not i in (E \ E') \/ (E' \ E) ; :: thesis: y in ((rng (g | (E /\ E'))) \/ (rng (g | (E \ E')))) \/ (rng (g | (E' \ E)))

A61: (E \/ E') \ (E \+\ E') = ((E \/ E') \ (E \/ E')) \/ (((E \/ E') /\ E) /\ E') by XBOOLE_1:102
.= {} \/ (((E \/ E') /\ E) /\ E') by XBOOLE_1:37
.= (E \/ E') /\ (E /\ E') by XBOOLE_1:16 ;
i in (E \/ E') \ (E \+\ E') by A51, A52, A60, XBOOLE_0:def 5;
then A62: i in dom (g | (E /\ E')) by A51, A61, RELAT_1:90;
then (g | (E /\ E')) . i = y by A53, FUNCT_1:70;
then y in rng (g | (E /\ E')) by A62, FUNCT_1:def 5;
then y in (rng (g | (E /\ E'))) \/ (rng (g | (E \ E'))) by XBOOLE_0:def 3;
hence y in ((rng (g | (E /\ E'))) \/ (rng (g | (E \ E')))) \/ (rng (g | (E' \ E))) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

rng (g | (E' \ E)) c= rng g by RELAT_1:99;
hence ((rng (g | (E /\ E'))) \/ (rng (g | (E \ E')))) \/ (rng (g | (E' \ E))) c= rng g by A50, XBOOLE_1:8; :: thesis: verum

end;

then A63: rng g = ((rng (g | (E /\ E'))) \/ (rng (g | (E \ E')))) \/ (rng (g | (E' \ E))) by A8;
A64: dom (g | (E' \ E)) = (dom g) /\ (E' \ E) by RELAT_1:90
.= (E \/ E') /\ (E' \ E) by FUNCT_2:def 1
.= ((E \/ E') /\ E') \ E by XBOOLE_1:49
.= E' \ E by XBOOLE_1:21 ;
A65: for i being set st i in dom (g | (E' \ E)) holds
(g | (E' \ E)) . i = f' . i

proof

let i be set ; :: thesis: ( i in dom (g | (E' \ E)) implies (g | (E' \ E)) . i = f' . i )
assume A66: i in dom (g | (E' \ E)) ; :: thesis: (g | (E' \ E)) . i = f' . i
then A67: i in (E \ E') \/ (E' \ E) by A64, XBOOLE_0:def 3;
not i in E by A64, A66, XBOOLE_0:def 5;
then f' . i = h . i by A7, A66
.= g . i by A8, A66, A67 ;
hence (g | (E' \ E)) . i = f' . i by A66, FUNCT_1:70; :: thesis: verum

end;

dom (g | (E' \ E)) = (E' /\ E') \ E by A64
.= E' /\ (E' \ E) by XBOOLE_1:49
.= (dom f') /\ (E' \ E) by FUNCT_2:def 1 ;
then A68: meet (rng (g | (E' \ E))) = meet (rng (f' | (E' \ E))) by A65, FUNCT_1:68;
A69: dom (g | (E \ E')) = (dom g) /\ (E \ E') by RELAT_1:90
.= (E \/ E') /\ (E \ E') by FUNCT_2:def 1
.= ((E \/ E') /\ E) \ E' by XBOOLE_1:49
.= E \ E' by XBOOLE_1:21 ;
A70: for i being set st i in dom (g | (E \ E')) holds
(g | (E \ E')) . i = f . i

proof

let i be set ; :: thesis: ( i in dom (g | (E \ E')) implies (g | (E \ E')) . i = f . i )
A71: E \ E' c= E by XBOOLE_1:36;
assume A72: i in dom (g | (E \ E')) ; :: thesis: (g | (E \ E')) . i = f . i
then i in (E \ E') \/ (E' \ E) by A69, XBOOLE_0:def 3;
then g . i = h . i by A8, A72
.= f . i by A7, A69, A72, A71 ;
hence (g | (E \ E')) . i = f . i by A72, FUNCT_1:70; :: thesis: verum

end;

dom (g | (E \ E')) = (E /\ E) \ E' by A69
.= E /\ (E \ E') by XBOOLE_1:49
.= (dom f) /\ (E \ E') by FUNCT_2:def 1 ;
then A73: meet (rng (g | (E \ E'))) = meet (rng (f | (E \ E'))) by A70, FUNCT_1:68;

per cases ( E /\ E' = {} or not E /\ E' = {} ) ;

suppose A74: E /\ E' = {} ; :: thesis: x /\ X = meet (rng g)

A75: E \ E' c= E by XBOOLE_1:36;
A76: ( E' c= dom g & E c= dom g ) by A8, XBOOLE_1:7;
A77: E' \ E c= E' by XBOOLE_1:36;
A78: E misses E' by A74, XBOOLE_0:def 7;
then A79: ( f | (E \ E') = f & f' | (E' \ E) = f' ) by RELSET_1:34, XBOOLE_1:86;
E c= E \ E' by A78, XBOOLE_1:86;
then A80: E = E \ E' by A75, XBOOLE_0:def 10;
E' c= E' \ E by A78, XBOOLE_1:86;
then A81: E' = E' \ E by A77, XBOOLE_0:def 10;
rng (g | (E /\ E')) = {} by A74;
hence x /\ X = meet (rng g) by A4, A6, A73, A68, A63, A79, A81, A80, A76, SETFAM_1:10; :: thesis: verum

end;

suppose A82: not E /\ E' = {} ; :: thesis: x /\ X = meet (rng g)

meet (rng g) = (meet (rng f)) /\ (meet (rng f'))

proof

per cases ( E \ E' = {} or not E \ E' = {} ) ;

suppose A83: E \ E' = {} ; :: thesis: meet (rng g) = (meet (rng f)) /\ (meet (rng f'))

then A84: rng (g | (E \ E')) = {} ;
A85: E c= E' by A83, XBOOLE_1:37;
A86: E /\ E' c= dom g by A8, XBOOLE_1:29;
meet (rng g) = (meet (rng f)) /\ (meet (rng f'))

proof

per cases ( E' \ E = {} or E' \ E <> {} ) ;

suppose E' \ E = {} ; :: thesis: meet (rng g) = (meet (rng f)) /\ (meet (rng f'))

then E' c= E by XBOOLE_1:37;
then A87: E = E' by A85, XBOOLE_0:def 10;
f | E = f by RELSET_1:34;
hence meet (rng g) = (meet (rng f)) /\ (meet (rng f')) by A17, A63, A84, A87, RELSET_1:34; :: thesis: verum

end;

suppose A88: E' \ E <> {} ; :: thesis: meet (rng g) = (meet (rng f)) /\ (meet (rng f'))

( E' \ E c= E' & E' c= E' \/ E ) by XBOOLE_1:7, XBOOLE_1:36;
then E' \ E c= dom g by A8, XBOOLE_1:1;
then meet (rng g) = (meet (rng (g | (E /\ E')))) /\ (meet (rng (g | (E' \ E)))) by A63, A82, A84, A86, A88, SETFAM_1:10;
then A89: meet (rng g) = ((meet (rng f)) /\ (meet (rng (f' | (E /\ E'))))) /\ (meet (rng (f' | (E' \ E)))) by A17, A68, A85, RELSET_1:34, XBOOLE_1:19;
A90: rng (f' | (E \ E')) = {} by A83;
E' \ E c= E' by XBOOLE_1:36;
then A91: E' \ E c= dom f' by FUNCT_2:def 1;
E /\ E' c= E' by XBOOLE_1:17;
then A92: E /\ E' c= dom f' by FUNCT_2:def 1;
( E' \/ E = E' & dom f' = E' ) by A85, FUNCT_2:def 1, XBOOLE_1:12;
then rng f' = ((rng (f' | (E /\ E'))) \/ (rng (f' | (E \ E')))) \/ (rng (f' | (E' \ E))) by A49
.= (rng (f' | (E /\ E'))) \/ (rng (f' | (E' \ E))) by A90 ;
then meet (rng f') = (meet (rng (f' | (E /\ E')))) /\ (meet (rng (f' | (E' \ E)))) by A82, A88, A92, A91, SETFAM_1:10;
hence meet (rng g) = (meet (rng f)) /\ (meet (rng f')) by A89, XBOOLE_1:16; :: thesis: verum

end;

end;

end;

hence meet (rng g) = (meet (rng f)) /\ (meet (rng f')) ; :: thesis: verum

end;

suppose A93: not E \ E' = {} ; :: thesis: meet (rng g) = (meet (rng f)) /\ (meet (rng f'))

meet (rng g) = (meet (rng f)) /\ (meet (rng f'))

proof

( E \ E' c= E & E c= dom g ) by A8, XBOOLE_1:7, XBOOLE_1:36;
then A94: rng (g | (E \ E')) <> {} by A93, Th1, XBOOLE_1:1;
A95: E /\ E' c= E \/ E' by XBOOLE_1:29;

per cases ( E' \ E = {} or not E' \ E = {} ) ;

suppose A96: E' \ E = {} ; :: thesis: meet (rng g) = (meet (rng f)) /\ (meet (rng f'))

then A97: rng (f | (E' \ E)) = {} ;
E' c= E by A96, XBOOLE_1:37;
then E = E \/ E' by XBOOLE_1:12;
then dom f = E \/ E' by FUNCT_2:def 1;
then A98: rng f = ((rng (f | (E /\ E'))) \/ (rng (f | (E \ E')))) \/ (rng (f | (E' \ E))) by A49
.= (rng (f | (E /\ E'))) \/ (rng (f | (E \ E'))) by A97 ;
E \ E' c= E by XBOOLE_1:36;
then A99: E \ E' c= dom f by FUNCT_2:def 1;
E' c= E by A96, XBOOLE_1:37;
then A100: f' | (E /\ E') = f' by RELSET_1:34, XBOOLE_1:19;
dom f = E by FUNCT_2:def 1;
then A101: rng (f | (E /\ E')) <> {} by A82, Th1, XBOOLE_1:17;
rng (g | (E' \ E)) = {} by A96;
then meet (rng g) = (meet (rng (g | (E /\ E')))) /\ (meet (rng (g | (E \ E')))) by A8, A63, A82, A95, A94, SETFAM_1:10
.= ((meet (rng (f | (E /\ E')))) /\ (meet (rng (f | (E \ E'))))) /\ (meet (rng (f' | (E /\ E')))) by A17, A73, XBOOLE_1:16 ;
hence meet (rng g) = (meet (rng f)) /\ (meet (rng f')) by A93, A100, A98, A101, A99, SETFAM_1:10; :: thesis: verum

end;

suppose A102: not E' \ E = {} ; :: thesis: meet (rng g) = (meet (rng f)) /\ (meet (rng f'))

( E' \ E c= E' & E' c= E \/ E' ) by XBOOLE_1:7, XBOOLE_1:36;
then E' \ E c= dom g by A8, XBOOLE_1:1;
then meet (rng g) = (meet ((rng (g | (E /\ E'))) \/ (rng (g | (E \ E'))))) /\ (meet (rng (g | (E' \ E)))) by A8, A63, A82, A95, A102, SETFAM_1:10
.= ((meet (rng (g | (E /\ E')))) /\ (meet (rng (g | (E \ E'))))) /\ (meet (rng (g | (E' \ E)))) by A8, A82, A95, A94, SETFAM_1:10 ;
then A103: meet (rng g) = (((meet (rng (f | (E /\ E')))) /\ (meet (rng (f | (E \ E'))))) /\ (meet (rng (f' | (E /\ E'))))) /\ (meet (rng (f' | (E' \ E)))) by A17, A73, A68, XBOOLE_1:16;
E /\ E' c= E by XBOOLE_1:17;
then A104: E /\ E' c= dom f by FUNCT_2:def 1;
E \/ (E /\ E') = E by XBOOLE_1:12, XBOOLE_1:17;
then dom f = E \/ (E /\ E') by FUNCT_2:def 1;
then A105: rng f = ((rng (f | (E /\ (E /\ E')))) \/ (rng (f | (E \ (E /\ E'))))) \/ (rng (f | ((E /\ E') \ E))) by A49;
E /\ E' c= E by XBOOLE_1:17;
then (E /\ E') \ E = {} by XBOOLE_1:37;
then A106: rng (f | ((E /\ E') \ E)) = {} ;
E' \ E c= E' by XBOOLE_1:36;
then A107: E' \ E c= dom f' by FUNCT_2:def 1;
E /\ E' c= E' by XBOOLE_1:17;
then A108: E /\ E' c= dom f' by FUNCT_2:def 1;
E /\ E' c= E' by XBOOLE_1:17;
then A109: ( E' \ E = E' \ (E /\ E') & (E /\ E') \ E' = {} ) by XBOOLE_1:37, XBOOLE_1:47;
E' \/ (E /\ E') = E' by XBOOLE_1:12, XBOOLE_1:17;
then A110: dom f' = E' \/ (E /\ E') by FUNCT_2:def 1;
E' /\ (E /\ E') = (E' /\ E') /\ E by XBOOLE_1:16
.= E /\ E' ;
then rng f' = ((rng (f' | (E /\ E'))) \/ (rng (f' | (E' \ E)))) \/ (rng (f' | {} )) by A49, A110, A109;
then A111: meet (rng f') = (meet (rng (f' | (E /\ E')))) /\ (meet (rng (f' | (E' \ E)))) by A82, A102, A108, A107, SETFAM_1:10;
E \ E' c= E by XBOOLE_1:36;
then A112: E \ E' c= dom f by FUNCT_2:def 1;
E /\ (E /\ E') = (E /\ E) /\ E' by XBOOLE_1:16
.= E /\ E' ;
then rng f = (rng (f | (E /\ E'))) \/ (rng (f | (E \ E'))) by A105, A106, XBOOLE_1:47;
then meet (rng f) = (meet (rng (f | (E /\ E')))) /\ (meet (rng (f | (E \ E')))) by A82, A93, A104, A112, SETFAM_1:10;
hence meet (rng g) = (meet (rng f)) /\ (meet (rng f')) by A111, A103, XBOOLE_1:16; :: thesis: verum

end;

end;

end;

hence meet (rng g) = (meet (rng f)) /\ (meet (rng f')) ; :: thesis: verum

end;

end;

end;

hence x /\ X = meet (rng g) by A4, A6; :: thesis: verum

end;

end;

end;

for y being set st y in (meet (rng f)) /\ (meet (rng f')) holds
y in Omega

proof

let y be set ; :: thesis: ( y in (meet (rng f)) /\ (meet (rng f')) implies y in Omega )
consider S being set such that
A113: S in rng f by XBOOLE_0:def 1;
consider S' being set such that
A114: S' in rng f' by XBOOLE_0:def 1;
assume A115: y in (meet (rng f)) /\ (meet (rng f')) ; :: thesis: y in Omega
then y in meet (rng f') by XBOOLE_0:def 4;
then A116: y in S' by A114, SETFAM_1:def 1;
y in meet (rng f) by A115, XBOOLE_0:def 4;
then y in S by A113, SETFAM_1:def 1;
then A117: y in S /\ S' by A116, XBOOLE_0:def 4;
S /\ S' is Event of Sigma by A113, A114, PROB_1:49;
hence y in Omega by A117; :: thesis: verum

end;

then reconsider xX = x /\ X as Subset of by A4, A6, TARSKI:def 3;
E \/ E' c= J by A3, A5, XBOOLE_1:8;
then xX in MeetSections J,F by A16, Def9;
hence x /\ X in MeetSections J,F ; :: thesis: verum

end;

hence MeetSections J,F is intersection_stable by FINSUB_1:def 2; :: thesis: verum