for x, X being set st x in MeetSections (J,F) & X in MeetSections (J,F) holds

x /\ X in MeetSections (J,F)

x /\ X in MeetSections (J,F)

proof

hence
MeetSections (J,F) is intersection_stable
by FINSUB_1:def 2; :: thesis: verum
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 I, f being SigmaSection of E,F such that

A3: E c= J and

A4: x = meet (rng f) by A1, Def9;

defpred S_{1}[ object ] means I in E;

deffunc H_{1}( object ) -> set = f . I;

consider E9 being non empty finite Subset of I, f9 being SigmaSection of E9,F such that

A5: E9 c= J and

A6: X = meet (rng f9) by A2, Def9;

deffunc H_{2}( object ) -> set = f9 . I;

defpred S_{2}[ object ] means I in (E \ E9) \/ (E9 \ E);

deffunc H_{3}( object ) -> set = (f . I) /\ (f9 . I);

consider h being Function such that

A7: ( dom h = E \/ E9 & ( for i being object st i in E \/ E9 holds

( ( S_{1}[i] implies h . i = H_{1}(i) ) & ( not S_{1}[i] implies h . i = H_{2}(i) ) ) ) )
from PARTFUN1:sch 1();

deffunc H_{4}( object ) -> set = h . I;

consider g being Function such that

A8: ( dom g = E \/ E9 & ( for i being object st i in E \/ E9 holds

( ( S_{2}[i] implies g . i = H_{4}(i) ) & ( not S_{2}[i] implies g . i = H_{3}(i) ) ) ) )
from PARTFUN1:sch 1();

A9: for i being set st i in E \/ E9 holds

g . i in F . i

then reconsider g = g as SigmaSection of E \/ E9,F by A9, Def4;

A16: x /\ X = meet (rng g)

y in Omega

E \/ E9 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;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 I, f being SigmaSection of E,F such that

A3: E c= J and

A4: x = meet (rng f) by A1, Def9;

defpred S

deffunc H

consider E9 being non empty finite Subset of I, f9 being SigmaSection of E9,F such that

A5: E9 c= J and

A6: X = meet (rng f9) by A2, Def9;

deffunc H

defpred S

deffunc H

consider h being Function such that

A7: ( dom h = E \/ E9 & ( for i being object st i in E \/ E9 holds

( ( S

deffunc H

consider g being Function such that

A8: ( dom g = E \/ E9 & ( for i being object st i in E \/ E9 holds

( ( S

A9: for i being set st i in E \/ E9 holds

g . i in F . i

proof

rng g c= Sigma
let i be set ; :: thesis: ( i in E \/ E9 implies g . i in F . i )

assume A10: i in E \/ E9 ; :: thesis: g . i in F . i

end;assume A10: i in E \/ E9 ; :: thesis: g . i in F . i

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

end;

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

h . i in F . i

end;proof end;

hence
g . i in F . i
by A8, A10, A11; :: thesis: verumsuppose A13:
not i in (E \ E9) \/ (E9 \ E)
; :: thesis: g . i in F . i

reconsider Fi = F . i as SigmaField of Omega by A10, Def2;

not i in E \+\ E9 by A13;

then ( i in E iff i in E9 ) by XBOOLE_0:1;

then ( f . i in F . i & f9 . i in F . i ) by A10, Def4, XBOOLE_0:def 3;

then A14: (f . i) /\ (f9 . i) is Event of Fi by PROB_1:19;

g . i = (f . i) /\ (f9 . i) by A8, A10, A13;

hence g . i in F . i by A14; :: thesis: verum

end;not i in E \+\ E9 by A13;

then ( i in E iff i in E9 ) by XBOOLE_0:1;

then ( f . i in F . i & f9 . i in F . i ) by A10, Def4, XBOOLE_0:def 3;

then A14: (f . i) /\ (f9 . i) is Event of Fi by PROB_1:19;

g . i = (f . i) /\ (f9 . i) by A8, A10, A13;

hence g . i in F . i by A14; :: thesis: verum

proof

then
g is Function of (E \/ E9),Sigma
by A8, FUNCT_2:2;
let y be object ; :: 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 object such that

A15: ( i in dom g & y = g . i ) by FUNCT_1:def 3;

( y in F . i & F . i in bool Sigma ) by A8, A9, A15, FUNCT_2:5;

hence y in Sigma ; :: thesis: verum

end;assume y in rng g ; :: thesis: y in Sigma

then consider i being object such that

A15: ( i in dom g & y = g . i ) by FUNCT_1:def 3;

( y in F . i & F . i in bool Sigma ) by A8, A9, A15, FUNCT_2:5;

hence y in Sigma ; :: thesis: verum

then reconsider g = g as SigmaSection of E \/ E9,F by A9, Def4;

A16: x /\ X = meet (rng g)

proof

for y being object st y in (meet (rng f)) /\ (meet (rng f9)) holds
A17:
meet (rng (g | (E /\ E9))) = (meet (rng (f | (E /\ E9)))) /\ (meet (rng (f9 | (E /\ E9))))

for g being Function st dom g = E \/ E9 holds

rng g = ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E)))

A64: dom (g | (E9 \ E)) = (dom g) /\ (E9 \ E) by RELAT_1:61

.= (E \/ E9) /\ (E9 \ E) by FUNCT_2:def 1

.= ((E \/ E9) /\ E9) \ E by XBOOLE_1:49

.= E9 \ E by XBOOLE_1:21 ;

A65: for i being object st i in dom (g | (E9 \ E)) holds

(g | (E9 \ E)) . i = f9 . i

.= E9 /\ (E9 \ E) by XBOOLE_1:49

.= (dom f9) /\ (E9 \ E) by FUNCT_2:def 1 ;

then A68: meet (rng (g | (E9 \ E))) = meet (rng (f9 | (E9 \ E))) by A65, FUNCT_1:46;

A69: dom (g | (E \ E9)) = (dom g) /\ (E \ E9) by RELAT_1:61

.= (E \/ E9) /\ (E \ E9) by FUNCT_2:def 1

.= ((E \/ E9) /\ E) \ E9 by XBOOLE_1:49

.= E \ E9 by XBOOLE_1:21 ;

A70: for i being object st i in dom (g | (E \ E9)) holds

(g | (E \ E9)) . i = f . i

.= E /\ (E \ E9) by XBOOLE_1:49

.= (dom f) /\ (E \ E9) by FUNCT_2:def 1 ;

then A73: meet (rng (g | (E \ E9))) = meet (rng (f | (E \ E9))) by A70, FUNCT_1:46;

end;proof
end;

A49:
for E, E9 being set per cases
( E /\ E9 = {} or not E /\ E9 = {} )
;

end;

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

then A19:
( meet (rng (f | (E /\ E9))) = meet (rng {}) & meet (rng (f9 | (E /\ E9))) = meet (rng {}) )
;

meet (rng (g | (E /\ E9))) = meet (rng {}) by A18

.= {} by SETFAM_1:def 1 ;

hence meet (rng (g | (E /\ E9))) = (meet (rng (f | (E /\ E9)))) /\ (meet (rng (f9 | (E /\ E9)))) by A19, SETFAM_1:def 1; :: thesis: verum

end;meet (rng (g | (E /\ E9))) = meet (rng {}) by A18

.= {} by SETFAM_1:def 1 ;

hence meet (rng (g | (E /\ E9))) = (meet (rng (f | (E /\ E9)))) /\ (meet (rng (f9 | (E /\ E9)))) by A19, SETFAM_1:def 1; :: thesis: verum

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

then reconsider EnE9 = E /\ E9 as non empty set ;

reconsider EE9 = EnE9 as Element of Fin EnE9 by FINSUB_1:def 5;

for B being Element of Fin EnE9 holds meet (rng (g | B)) = (meet (rng (f | B))) /\ (meet (rng (f9 | B)))

hence meet (rng (g | (E /\ E9))) = (meet (rng (f | (E /\ E9)))) /\ (meet (rng (f9 | (E /\ E9)))) ; :: thesis: verum

end;reconsider EE9 = EnE9 as Element of Fin EnE9 by FINSUB_1:def 5;

for B being Element of Fin EnE9 holds meet (rng (g | B)) = (meet (rng (f | B))) /\ (meet (rng (f9 | B)))

proof

then
meet (rng (g | EE9)) = (meet (rng (f | EE9))) /\ (meet (rng (f9 | EE9)))
;
defpred S_{3}[ set ] means meet (rng (g | I)) = (meet (rng (f | I))) /\ (meet (rng (f9 | I)));

let B be Element of Fin EnE9; :: thesis: meet (rng (g | B)) = (meet (rng (f | B))) /\ (meet (rng (f9 | B)))

A20: for B9 being Element of Fin EnE9

for b being Element of EnE9 st S_{3}[B9] & not b in B9 holds

S_{3}[B9 \/ {b}]
_{3}[ {}. EnE9]
;

for B1 being Element of Fin EnE9 holds S_{3}[B1]
from SETWISEO:sch 2(A48, A20);

hence meet (rng (g | B)) = (meet (rng (f | B))) /\ (meet (rng (f9 | B))) ; :: thesis: verum

end;let B be Element of Fin EnE9; :: thesis: meet (rng (g | B)) = (meet (rng (f | B))) /\ (meet (rng (f9 | B)))

A20: for B9 being Element of Fin EnE9

for b being Element of EnE9 st S

S

proof

A48:
S
let B9 be Element of Fin EnE9; :: thesis: for b being Element of EnE9 st S_{3}[B9] & not b in B9 holds

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

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

assume that

A21: meet (rng (g | B9)) = (meet (rng (f | B9))) /\ (meet (rng (f9 | B9))) and

not b in B9 ; :: thesis: S_{3}[B9 \/ {b}]

A22: dom (f | {b}) = (dom f) /\ {b} by RELAT_1:61;

dom f = E by FUNCT_2:def 1;

then A23: E /\ E9 c= dom f by XBOOLE_1:17;

then b in dom f ;

then A24: rng (f | {b}) = {((f | {b}) . b)} by A22, FUNCT_1:4, ZFMISC_1:46;

b in (E \ (E \/ E9)) \/ ((E /\ E) /\ E9) by XBOOLE_0:def 3;

then b in E \ (E \+\ E9) by XBOOLE_1:102;

then A25: not b in E \+\ E9 by XBOOLE_0:def 5;

A26: b in {b} by TARSKI:def 1;

b in dom f by A23;

then b in dom (f | {b}) by A26, RELAT_1:57;

then A27: rng (f | {b}) = {(f . b)} by A24, FUNCT_1:47;

then A28: meet (rng (f | {b})) = f . b by SETFAM_1:10;

A29: E /\ E9 c= E by XBOOLE_1:17;

A30: dom (f9 | {b}) = (dom f9) /\ {b} by RELAT_1:61;

dom f9 = E9 by FUNCT_2:def 1;

then A31: E /\ E9 c= dom f9 by XBOOLE_1:17;

then b in dom f9 ;

then A32: rng (f9 | {b}) = {((f9 | {b}) . b)} by A30, FUNCT_1:4, ZFMISC_1:46;

b in dom f9 by A31;

then b in dom (f9 | {b}) by A26, RELAT_1:57;

then A33: rng (f9 | {b}) = {(f9 . b)} by A32, FUNCT_1:47;

then A34: meet (rng (f9 | {b})) = f9 . b by SETFAM_1:10;

A35: for g being Function

for B9, b being set holds meet (rng (g | (B9 \/ {b}))) = meet ((rng (g | B9)) \/ (rng (g | {b})))

then A36: E /\ E9 c= dom g by A29;

then b is Element of dom g ;

then (dom g) /\ {b} = {b} by ZFMISC_1:46;

then dom (g | {b}) = {b} by RELAT_1:61;

then A37: rng (g | {b}) = {((g | {b}) . b)} by FUNCT_1:4;

( b in {b} & b in dom g ) by A36, TARSKI:def 1;

then b in dom (g | {b}) by RELAT_1:57;

then A38: rng (g | {b}) = {(g . b)} by A37, FUNCT_1:47;

then A39: meet (rng (g | {b})) = g . b by SETFAM_1:10;

E c= E \/ E9 by XBOOLE_1:7;

then A40: E /\ E9 c= E \/ E9 by A29;

then b in E \/ E9 ;

then A41: g . b = (f . b) /\ (f9 . b) by A8, A25;

end;S

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

assume that

A21: meet (rng (g | B9)) = (meet (rng (f | B9))) /\ (meet (rng (f9 | B9))) and

not b in B9 ; :: thesis: S

A22: dom (f | {b}) = (dom f) /\ {b} by RELAT_1:61;

dom f = E by FUNCT_2:def 1;

then A23: E /\ E9 c= dom f by XBOOLE_1:17;

then b in dom f ;

then A24: rng (f | {b}) = {((f | {b}) . b)} by A22, FUNCT_1:4, ZFMISC_1:46;

b in (E \ (E \/ E9)) \/ ((E /\ E) /\ E9) by XBOOLE_0:def 3;

then b in E \ (E \+\ E9) by XBOOLE_1:102;

then A25: not b in E \+\ E9 by XBOOLE_0:def 5;

A26: b in {b} by TARSKI:def 1;

b in dom f by A23;

then b in dom (f | {b}) by A26, RELAT_1:57;

then A27: rng (f | {b}) = {(f . b)} by A24, FUNCT_1:47;

then A28: meet (rng (f | {b})) = f . b by SETFAM_1:10;

A29: E /\ E9 c= E by XBOOLE_1:17;

A30: dom (f9 | {b}) = (dom f9) /\ {b} by RELAT_1:61;

dom f9 = E9 by FUNCT_2:def 1;

then A31: E /\ E9 c= dom f9 by XBOOLE_1:17;

then b in dom f9 ;

then A32: rng (f9 | {b}) = {((f9 | {b}) . b)} by A30, FUNCT_1:4, ZFMISC_1:46;

b in dom f9 by A31;

then b in dom (f9 | {b}) by A26, RELAT_1:57;

then A33: rng (f9 | {b}) = {(f9 . b)} by A32, FUNCT_1:47;

then A34: meet (rng (f9 | {b})) = f9 . b by SETFAM_1:10;

A35: for g being Function

for B9, b being set holds meet (rng (g | (B9 \/ {b}))) = meet ((rng (g | B9)) \/ (rng (g | {b})))

proof

E c= dom g
by A8, XBOOLE_1:7;
let g be Function; :: thesis: for B9, b being set holds meet (rng (g | (B9 \/ {b}))) = meet ((rng (g | B9)) \/ (rng (g | {b})))

let B9, b be set ; :: thesis: meet (rng (g | (B9 \/ {b}))) = meet ((rng (g | B9)) \/ (rng (g | {b})))

rng (g | (B9 \/ {b})) = rng ((g | B9) \/ (g | {b})) by RELAT_1:78;

hence meet (rng (g | (B9 \/ {b}))) = meet ((rng (g | B9)) \/ (rng (g | {b}))) by RELAT_1:12; :: thesis: verum

end;let B9, b be set ; :: thesis: meet (rng (g | (B9 \/ {b}))) = meet ((rng (g | B9)) \/ (rng (g | {b})))

rng (g | (B9 \/ {b})) = rng ((g | B9) \/ (g | {b})) by RELAT_1:78;

hence meet (rng (g | (B9 \/ {b}))) = meet ((rng (g | B9)) \/ (rng (g | {b}))) by RELAT_1:12; :: thesis: verum

then A36: E /\ E9 c= dom g by A29;

then b is Element of dom g ;

then (dom g) /\ {b} = {b} by ZFMISC_1:46;

then dom (g | {b}) = {b} by RELAT_1:61;

then A37: rng (g | {b}) = {((g | {b}) . b)} by FUNCT_1:4;

( b in {b} & b in dom g ) by A36, TARSKI:def 1;

then b in dom (g | {b}) by RELAT_1:57;

then A38: rng (g | {b}) = {(g . b)} by A37, FUNCT_1:47;

then A39: meet (rng (g | {b})) = g . b by SETFAM_1:10;

E c= E \/ E9 by XBOOLE_1:7;

then A40: E /\ E9 c= E \/ E9 by A29;

then b in E \/ E9 ;

then A41: g . b = (f . b) /\ (f9 . b) by A8, A25;

per cases
( B9 = {} or B9 <> {} )
;

end;

suppose A42:
B9 <> {}
; :: thesis: S_{3}[B9 \/ {b}]

set z = the Element of B9;

B9 c= E /\ E9 by FINSUB_1:def 5;

then A43: B9 c= E \/ E9 by A40;

the Element of B9 in B9 by A42;

then dom (g | B9) <> {} by A8, A43;

then rng (g | B9) <> {} by RELAT_1:42;

then meet ((rng (g | B9)) \/ (rng (g | {b}))) = (meet (rng (g | B9))) /\ (meet (rng (g | {b}))) by A37, SETFAM_1:9;

then A44: meet (rng (g | (B9 \/ {b}))) = ((meet (rng (f | B9))) /\ (meet (rng (f9 | B9)))) /\ (g . b) by A21, A35, A39

.= (meet (rng (f | B9))) /\ ((meet (rng (f9 | B9))) /\ ((f . b) /\ (f9 . b))) by A41, XBOOLE_1:16

.= (meet (rng (f | B9))) /\ ((f . b) /\ ((meet (rng (f9 | B9))) /\ (f9 . b))) by XBOOLE_1:16

.= ((meet (rng (f | B9))) /\ (f . b)) /\ ((meet (rng (f9 | B9))) /\ (f9 . b)) by XBOOLE_1:16 ;

( B9 c= E /\ E9 & E /\ E9 c= E9 ) by FINSUB_1:def 5, XBOOLE_1:17;

then B9 c= E9 ;

then A45: B9 c= dom f9 by FUNCT_2:def 1;

( B9 c= E /\ E9 & E /\ E9 c= E ) by FINSUB_1:def 5, XBOOLE_1:17;

then B9 c= E ;

then A46: B9 c= dom f by FUNCT_2:def 1;

meet (rng (f | (B9 \/ {b}))) = meet ((rng (f | B9)) \/ (rng (f | {b}))) by A35

.= (meet (rng (f | B9))) /\ (meet (rng (f | {b}))) by A24, A42, A46, SETFAM_1:9 ;

then A47: (meet (rng (f | B9))) /\ (f . b) = meet (rng (f | (B9 \/ {b}))) by A27, SETFAM_1:10;

meet (rng (f9 | (B9 \/ {b}))) = meet ((rng (f9 | B9)) \/ (rng (f9 | {b}))) by A35

.= (meet (rng (f9 | B9))) /\ (meet (rng (f9 | {b}))) by A32, A42, A45, SETFAM_1:9 ;

hence S_{3}[B9 \/ {b}]
by A33, A44, A47, SETFAM_1:10; :: thesis: verum

end;B9 c= E /\ E9 by FINSUB_1:def 5;

then A43: B9 c= E \/ E9 by A40;

the Element of B9 in B9 by A42;

then dom (g | B9) <> {} by A8, A43;

then rng (g | B9) <> {} by RELAT_1:42;

then meet ((rng (g | B9)) \/ (rng (g | {b}))) = (meet (rng (g | B9))) /\ (meet (rng (g | {b}))) by A37, SETFAM_1:9;

then A44: meet (rng (g | (B9 \/ {b}))) = ((meet (rng (f | B9))) /\ (meet (rng (f9 | B9)))) /\ (g . b) by A21, A35, A39

.= (meet (rng (f | B9))) /\ ((meet (rng (f9 | B9))) /\ ((f . b) /\ (f9 . b))) by A41, XBOOLE_1:16

.= (meet (rng (f | B9))) /\ ((f . b) /\ ((meet (rng (f9 | B9))) /\ (f9 . b))) by XBOOLE_1:16

.= ((meet (rng (f | B9))) /\ (f . b)) /\ ((meet (rng (f9 | B9))) /\ (f9 . b)) by XBOOLE_1:16 ;

( B9 c= E /\ E9 & E /\ E9 c= E9 ) by FINSUB_1:def 5, XBOOLE_1:17;

then B9 c= E9 ;

then A45: B9 c= dom f9 by FUNCT_2:def 1;

( B9 c= E /\ E9 & E /\ E9 c= E ) by FINSUB_1:def 5, XBOOLE_1:17;

then B9 c= E ;

then A46: B9 c= dom f by FUNCT_2:def 1;

meet (rng (f | (B9 \/ {b}))) = meet ((rng (f | B9)) \/ (rng (f | {b}))) by A35

.= (meet (rng (f | B9))) /\ (meet (rng (f | {b}))) by A24, A42, A46, SETFAM_1:9 ;

then A47: (meet (rng (f | B9))) /\ (f . b) = meet (rng (f | (B9 \/ {b}))) by A27, SETFAM_1:10;

meet (rng (f9 | (B9 \/ {b}))) = meet ((rng (f9 | B9)) \/ (rng (f9 | {b}))) by A35

.= (meet (rng (f9 | B9))) /\ (meet (rng (f9 | {b}))) by A32, A42, A45, SETFAM_1:9 ;

hence S

for B1 being Element of Fin EnE9 holds S

hence meet (rng (g | B)) = (meet (rng (f | B))) /\ (meet (rng (f9 | B))) ; :: thesis: verum

hence meet (rng (g | (E /\ E9))) = (meet (rng (f | (E /\ E9)))) /\ (meet (rng (f9 | (E /\ E9)))) ; :: thesis: verum

for g being Function st dom g = E \/ E9 holds

rng g = ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E)))

proof

then A63:
rng g = ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E)))
by A8;
let E, E9 be set ; :: thesis: for g being Function st dom g = E \/ E9 holds

rng g = ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E)))

let g be Function; :: thesis: ( dom g = E \/ E9 implies rng g = ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E))) )

( rng (g | (E /\ E9)) c= rng g & rng (g | (E \ E9)) c= rng g ) by RELAT_1:70;

then A50: (rng (g | (E /\ E9))) \/ (rng (g | (E \ E9))) c= rng g by XBOOLE_1:8;

assume A51: dom g = E \/ E9 ; :: thesis: rng g = ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E)))

thus rng g c= ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E))) :: according to XBOOLE_0:def 10 :: thesis: ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E))) c= rng g

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

end;rng g = ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E)))

let g be Function; :: thesis: ( dom g = E \/ E9 implies rng g = ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E))) )

( rng (g | (E /\ E9)) c= rng g & rng (g | (E \ E9)) c= rng g ) by RELAT_1:70;

then A50: (rng (g | (E /\ E9))) \/ (rng (g | (E \ E9))) c= rng g by XBOOLE_1:8;

assume A51: dom g = E \/ E9 ; :: thesis: rng g = ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E)))

thus rng g c= ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E))) :: according to XBOOLE_0:def 10 :: thesis: ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E))) c= rng g

proof

rng (g | (E9 \ E)) c= rng g
by RELAT_1:70;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng g or y in ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E))) )

assume y in rng g ; :: thesis: y in ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E)))

then consider i being object such that

A52: i in dom g and

A53: y = g . i by FUNCT_1:def 3;

end;assume y in rng g ; :: thesis: y in ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E)))

then consider i being object such that

A52: i in dom g and

A53: y = g . i by FUNCT_1:def 3;

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

end;

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

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

end;proof
end;

hence
y in ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E)))
; :: thesis: verumper cases
( i in E or not i in E )
;

end;

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

A56:
E /\ E9 c= E
by XBOOLE_1:17;

E /\ ((E \ E9) \/ (E9 \ E)) = (E /\ (E \ E9)) \/ (E /\ (E9 \ E)) by XBOOLE_1:23

.= (E \ E9) \/ (E /\ (E9 \ E)) by XBOOLE_1:28

.= (E \ E9) \/ ((E /\ E9) \ E) by XBOOLE_1:49

.= (E \ E9) \/ {} by A56, XBOOLE_1:37 ;

then i in E \ E9 by A54, A55, XBOOLE_0:def 4;

then i in (dom g) /\ (E \ E9) by A52, XBOOLE_0:def 4;

then A57: i in dom (g | (E \ E9)) by RELAT_1:61;

then (g | (E \ E9)) . i = y by A53, FUNCT_1:47;

then y in rng (g | (E \ E9)) by A57, FUNCT_1:def 3;

then y in (rng (g | (E /\ E9))) \/ (rng (g | (E \ E9))) by XBOOLE_0:def 3;

hence y in ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E))) by XBOOLE_0:def 3; :: thesis: verum

end;E /\ ((E \ E9) \/ (E9 \ E)) = (E /\ (E \ E9)) \/ (E /\ (E9 \ E)) by XBOOLE_1:23

.= (E \ E9) \/ (E /\ (E9 \ E)) by XBOOLE_1:28

.= (E \ E9) \/ ((E /\ E9) \ E) by XBOOLE_1:49

.= (E \ E9) \/ {} by A56, XBOOLE_1:37 ;

then i in E \ E9 by A54, A55, XBOOLE_0:def 4;

then i in (dom g) /\ (E \ E9) by A52, XBOOLE_0:def 4;

then A57: i in dom (g | (E \ E9)) by RELAT_1:61;

then (g | (E \ E9)) . i = y by A53, FUNCT_1:47;

then y in rng (g | (E \ E9)) by A57, FUNCT_1:def 3;

then y in (rng (g | (E /\ E9))) \/ (rng (g | (E \ E9))) by XBOOLE_0:def 3;

hence y in ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E))) by XBOOLE_0:def 3; :: thesis: verum

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

((E \ E9) \/ (E9 \ E)) \ E =
((E \ E9) \ E) \/ ((E9 \ E) \ E)
by XBOOLE_1:42

.= {} \/ ((E9 \ E) \ E) by XBOOLE_1:37

.= E9 \ (E \/ E) by XBOOLE_1:41 ;

then i in E9 \ (E \/ E) by A54, A58, XBOOLE_0:def 5;

then i in (dom g) /\ (E9 \ E) by A52, XBOOLE_0:def 4;

then A59: i in dom (g | (E9 \ E)) by RELAT_1:61;

then (g | (E9 \ E)) . i = y by A53, FUNCT_1:47;

then y in rng (g | (E9 \ E)) by A59, FUNCT_1:def 3;

then y in (rng (g | (E \ E9))) \/ (rng (g | (E9 \ E))) by XBOOLE_0:def 3;

then y in (rng (g | (E /\ E9))) \/ ((rng (g | (E \ E9))) \/ (rng (g | (E9 \ E)))) by XBOOLE_0:def 3;

hence y in ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E))) by XBOOLE_1:4; :: thesis: verum

end;.= {} \/ ((E9 \ E) \ E) by XBOOLE_1:37

.= E9 \ (E \/ E) by XBOOLE_1:41 ;

then i in E9 \ (E \/ E) by A54, A58, XBOOLE_0:def 5;

then i in (dom g) /\ (E9 \ E) by A52, XBOOLE_0:def 4;

then A59: i in dom (g | (E9 \ E)) by RELAT_1:61;

then (g | (E9 \ E)) . i = y by A53, FUNCT_1:47;

then y in rng (g | (E9 \ E)) by A59, FUNCT_1:def 3;

then y in (rng (g | (E \ E9))) \/ (rng (g | (E9 \ E))) by XBOOLE_0:def 3;

then y in (rng (g | (E /\ E9))) \/ ((rng (g | (E \ E9))) \/ (rng (g | (E9 \ E)))) by XBOOLE_0:def 3;

hence y in ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E))) by XBOOLE_1:4; :: thesis: verum

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

A61: (E \/ E9) \ (E \+\ E9) =
((E \/ E9) \ (E \/ E9)) \/ (((E \/ E9) /\ E) /\ E9)
by XBOOLE_1:102

.= {} \/ (((E \/ E9) /\ E) /\ E9) by XBOOLE_1:37

.= (E \/ E9) /\ (E /\ E9) by XBOOLE_1:16 ;

i in (E \/ E9) \ (E \+\ E9) by A51, A52, A60, XBOOLE_0:def 5;

then A62: i in dom (g | (E /\ E9)) by A51, A61, RELAT_1:61;

then (g | (E /\ E9)) . i = y by A53, FUNCT_1:47;

then y in rng (g | (E /\ E9)) by A62, FUNCT_1:def 3;

then y in (rng (g | (E /\ E9))) \/ (rng (g | (E \ E9))) by XBOOLE_0:def 3;

hence y in ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E))) by XBOOLE_0:def 3; :: thesis: verum

end;.= {} \/ (((E \/ E9) /\ E) /\ E9) by XBOOLE_1:37

.= (E \/ E9) /\ (E /\ E9) by XBOOLE_1:16 ;

i in (E \/ E9) \ (E \+\ E9) by A51, A52, A60, XBOOLE_0:def 5;

then A62: i in dom (g | (E /\ E9)) by A51, A61, RELAT_1:61;

then (g | (E /\ E9)) . i = y by A53, FUNCT_1:47;

then y in rng (g | (E /\ E9)) by A62, FUNCT_1:def 3;

then y in (rng (g | (E /\ E9))) \/ (rng (g | (E \ E9))) by XBOOLE_0:def 3;

hence y in ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E))) by XBOOLE_0:def 3; :: thesis: verum

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

A64: dom (g | (E9 \ E)) = (dom g) /\ (E9 \ E) by RELAT_1:61

.= (E \/ E9) /\ (E9 \ E) by FUNCT_2:def 1

.= ((E \/ E9) /\ E9) \ E by XBOOLE_1:49

.= E9 \ E by XBOOLE_1:21 ;

A65: for i being object st i in dom (g | (E9 \ E)) holds

(g | (E9 \ E)) . i = f9 . i

proof

dom (g | (E9 \ E)) =
(E9 /\ E9) \ E
by A64
let i be object ; :: thesis: ( i in dom (g | (E9 \ E)) implies (g | (E9 \ E)) . i = f9 . i )

assume A66: i in dom (g | (E9 \ E)) ; :: thesis: (g | (E9 \ E)) . i = f9 . i

then A67: i in (E \ E9) \/ (E9 \ E) by A64, XBOOLE_0:def 3;

not i in E by A64, A66, XBOOLE_0:def 5;

then f9 . i = h . i by A7, A66

.= g . i by A8, A66, A67 ;

hence (g | (E9 \ E)) . i = f9 . i by A66, FUNCT_1:47; :: thesis: verum

end;assume A66: i in dom (g | (E9 \ E)) ; :: thesis: (g | (E9 \ E)) . i = f9 . i

then A67: i in (E \ E9) \/ (E9 \ E) by A64, XBOOLE_0:def 3;

not i in E by A64, A66, XBOOLE_0:def 5;

then f9 . i = h . i by A7, A66

.= g . i by A8, A66, A67 ;

hence (g | (E9 \ E)) . i = f9 . i by A66, FUNCT_1:47; :: thesis: verum

.= E9 /\ (E9 \ E) by XBOOLE_1:49

.= (dom f9) /\ (E9 \ E) by FUNCT_2:def 1 ;

then A68: meet (rng (g | (E9 \ E))) = meet (rng (f9 | (E9 \ E))) by A65, FUNCT_1:46;

A69: dom (g | (E \ E9)) = (dom g) /\ (E \ E9) by RELAT_1:61

.= (E \/ E9) /\ (E \ E9) by FUNCT_2:def 1

.= ((E \/ E9) /\ E) \ E9 by XBOOLE_1:49

.= E \ E9 by XBOOLE_1:21 ;

A70: for i being object st i in dom (g | (E \ E9)) holds

(g | (E \ E9)) . i = f . i

proof

dom (g | (E \ E9)) =
(E /\ E) \ E9
by A69
let i be object ; :: thesis: ( i in dom (g | (E \ E9)) implies (g | (E \ E9)) . i = f . i )

A71: E \ E9 c= E by XBOOLE_1:36;

assume A72: i in dom (g | (E \ E9)) ; :: thesis: (g | (E \ E9)) . i = f . i

then i in (E \ E9) \/ (E9 \ 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 \ E9)) . i = f . i by A72, FUNCT_1:47; :: thesis: verum

end;A71: E \ E9 c= E by XBOOLE_1:36;

assume A72: i in dom (g | (E \ E9)) ; :: thesis: (g | (E \ E9)) . i = f . i

then i in (E \ E9) \/ (E9 \ 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 \ E9)) . i = f . i by A72, FUNCT_1:47; :: thesis: verum

.= E /\ (E \ E9) by XBOOLE_1:49

.= (dom f) /\ (E \ E9) by FUNCT_2:def 1 ;

then A73: meet (rng (g | (E \ E9))) = meet (rng (f | (E \ E9))) by A70, FUNCT_1:46;

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

end;

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

A75:
E \ E9 c= E
by XBOOLE_1:36;

A76: ( E9 c= dom g & E c= dom g ) by A8, XBOOLE_1:7;

A77: E9 \ E c= E9 by XBOOLE_1:36;

A78: E misses E9 by A74;

E c= E \ E9 by A78, XBOOLE_1:86;

then A79: E = E \ E9 by A75;

E9 c= E9 \ E by A78, XBOOLE_1:86;

then A80: E9 = E9 \ E by A77;

rng (g | (E /\ E9)) = {} by A74;

hence x /\ X = meet (rng g) by A4, A6, A73, A68, A63, A80, A79, A76, SETFAM_1:9; :: thesis: verum

end;A76: ( E9 c= dom g & E c= dom g ) by A8, XBOOLE_1:7;

A77: E9 \ E c= E9 by XBOOLE_1:36;

A78: E misses E9 by A74;

E c= E \ E9 by A78, XBOOLE_1:86;

then A79: E = E \ E9 by A75;

E9 c= E9 \ E by A78, XBOOLE_1:86;

then A80: E9 = E9 \ E by A77;

rng (g | (E /\ E9)) = {} by A74;

hence x /\ X = meet (rng g) by A4, A6, A73, A68, A63, A80, A79, A76, SETFAM_1:9; :: thesis: verum

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

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

end;proof
end;

hence
x /\ X = meet (rng g)
by A4, A6; :: thesis: verumper cases
( E \ E9 = {} or not E \ E9 = {} )
;

end;

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

then A83:
rng (g | (E \ E9)) = {}
;

A84: E c= E9 by A82, XBOOLE_1:37;

A85: E /\ E9 c= dom g by A8, XBOOLE_1:29;

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

end;A84: E c= E9 by A82, XBOOLE_1:37;

A85: E /\ E9 c= dom g by A8, XBOOLE_1:29;

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

proof
end;

hence
meet (rng g) = (meet (rng f)) /\ (meet (rng f9))
; :: thesis: verumper cases
( E9 \ E = {} or E9 \ E <> {} )
;

end;

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

then
E9 c= E
by XBOOLE_1:37;

then A86: E = E9 by A84;

thus meet (rng g) = (meet (rng f)) /\ (meet (rng f9)) by A17, A86; :: thesis: verum

end;then A86: E = E9 by A84;

thus meet (rng g) = (meet (rng f)) /\ (meet (rng f9)) by A17, A86; :: thesis: verum

suppose A87:
E9 \ E <> {}
; :: thesis: meet (rng g) = (meet (rng f)) /\ (meet (rng f9))

( E9 \ E c= E9 & E9 c= E9 \/ E )
by XBOOLE_1:7, XBOOLE_1:36;

then E9 \ E c= dom g by A8;

then meet (rng g) = (meet (rng (g | (E /\ E9)))) /\ (meet (rng (g | (E9 \ E)))) by A63, A81, A83, A85, A87, SETFAM_1:9;

then A88: meet (rng g) = ((meet (rng f)) /\ (meet (rng (f9 | (E /\ E9))))) /\ (meet (rng (f9 | (E9 \ E)))) by A17, A68, A84, RELSET_1:19, XBOOLE_1:19;

A89: rng (f9 | (E \ E9)) = {} by A82;

E9 \ E c= E9 by XBOOLE_1:36;

then A90: E9 \ E c= dom f9 by FUNCT_2:def 1;

E /\ E9 c= E9 by XBOOLE_1:17;

then A91: E /\ E9 c= dom f9 by FUNCT_2:def 1;

( E9 \/ E = E9 & dom f9 = E9 ) by A84, FUNCT_2:def 1, XBOOLE_1:12;

then rng f9 = ((rng (f9 | (E /\ E9))) \/ (rng (f9 | (E \ E9)))) \/ (rng (f9 | (E9 \ E))) by A49

.= (rng (f9 | (E /\ E9))) \/ (rng (f9 | (E9 \ E))) by A89 ;

then meet (rng f9) = (meet (rng (f9 | (E /\ E9)))) /\ (meet (rng (f9 | (E9 \ E)))) by A81, A87, A91, A90, SETFAM_1:9;

hence meet (rng g) = (meet (rng f)) /\ (meet (rng f9)) by A88, XBOOLE_1:16; :: thesis: verum

end;then E9 \ E c= dom g by A8;

then meet (rng g) = (meet (rng (g | (E /\ E9)))) /\ (meet (rng (g | (E9 \ E)))) by A63, A81, A83, A85, A87, SETFAM_1:9;

then A88: meet (rng g) = ((meet (rng f)) /\ (meet (rng (f9 | (E /\ E9))))) /\ (meet (rng (f9 | (E9 \ E)))) by A17, A68, A84, RELSET_1:19, XBOOLE_1:19;

A89: rng (f9 | (E \ E9)) = {} by A82;

E9 \ E c= E9 by XBOOLE_1:36;

then A90: E9 \ E c= dom f9 by FUNCT_2:def 1;

E /\ E9 c= E9 by XBOOLE_1:17;

then A91: E /\ E9 c= dom f9 by FUNCT_2:def 1;

( E9 \/ E = E9 & dom f9 = E9 ) by A84, FUNCT_2:def 1, XBOOLE_1:12;

then rng f9 = ((rng (f9 | (E /\ E9))) \/ (rng (f9 | (E \ E9)))) \/ (rng (f9 | (E9 \ E))) by A49

.= (rng (f9 | (E /\ E9))) \/ (rng (f9 | (E9 \ E))) by A89 ;

then meet (rng f9) = (meet (rng (f9 | (E /\ E9)))) /\ (meet (rng (f9 | (E9 \ E)))) by A81, A87, A91, A90, SETFAM_1:9;

hence meet (rng g) = (meet (rng f)) /\ (meet (rng f9)) by A88, XBOOLE_1:16; :: thesis: verum

suppose A92:
not E \ E9 = {}
; :: thesis: meet (rng g) = (meet (rng f)) /\ (meet (rng f9))

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

end;proof

hence
meet (rng g) = (meet (rng f)) /\ (meet (rng f9))
; :: thesis: verum
( E \ E9 c= E & E c= dom g )
by A8, XBOOLE_1:7, XBOOLE_1:36;

then A93: rng (g | (E \ E9)) <> {} by A92, Th1, XBOOLE_1:1;

A94: E /\ E9 c= E \/ E9 by XBOOLE_1:29;

end;then A93: rng (g | (E \ E9)) <> {} by A92, Th1, XBOOLE_1:1;

A94: E /\ E9 c= E \/ E9 by XBOOLE_1:29;

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

end;

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

then A96:
rng (f | (E9 \ E)) = {}
;

E9 c= E by A95, XBOOLE_1:37;

then E = E \/ E9 by XBOOLE_1:12;

then dom f = E \/ E9 by FUNCT_2:def 1;

then A97: rng f = ((rng (f | (E /\ E9))) \/ (rng (f | (E \ E9)))) \/ (rng (f | (E9 \ E))) by A49

.= (rng (f | (E /\ E9))) \/ (rng (f | (E \ E9))) by A96 ;

E \ E9 c= E by XBOOLE_1:36;

then A98: E \ E9 c= dom f by FUNCT_2:def 1;

E9 c= E by A95, XBOOLE_1:37;

then A99: f9 | (E /\ E9) = f9 by RELSET_1:19, XBOOLE_1:19;

dom f = E by FUNCT_2:def 1;

then A100: rng (f | (E /\ E9)) <> {} by A81, Th1, XBOOLE_1:17;

rng (g | (E9 \ E)) = {} by A95;

then meet (rng g) = (meet (rng (g | (E /\ E9)))) /\ (meet (rng (g | (E \ E9)))) by A8, A63, A81, A94, A93, SETFAM_1:9

.= ((meet (rng (f | (E /\ E9)))) /\ (meet (rng (f | (E \ E9))))) /\ (meet (rng (f9 | (E /\ E9)))) by A17, A73, XBOOLE_1:16 ;

hence meet (rng g) = (meet (rng f)) /\ (meet (rng f9)) by A92, A99, A97, A100, A98, SETFAM_1:9; :: thesis: verum

end;E9 c= E by A95, XBOOLE_1:37;

then E = E \/ E9 by XBOOLE_1:12;

then dom f = E \/ E9 by FUNCT_2:def 1;

then A97: rng f = ((rng (f | (E /\ E9))) \/ (rng (f | (E \ E9)))) \/ (rng (f | (E9 \ E))) by A49

.= (rng (f | (E /\ E9))) \/ (rng (f | (E \ E9))) by A96 ;

E \ E9 c= E by XBOOLE_1:36;

then A98: E \ E9 c= dom f by FUNCT_2:def 1;

E9 c= E by A95, XBOOLE_1:37;

then A99: f9 | (E /\ E9) = f9 by RELSET_1:19, XBOOLE_1:19;

dom f = E by FUNCT_2:def 1;

then A100: rng (f | (E /\ E9)) <> {} by A81, Th1, XBOOLE_1:17;

rng (g | (E9 \ E)) = {} by A95;

then meet (rng g) = (meet (rng (g | (E /\ E9)))) /\ (meet (rng (g | (E \ E9)))) by A8, A63, A81, A94, A93, SETFAM_1:9

.= ((meet (rng (f | (E /\ E9)))) /\ (meet (rng (f | (E \ E9))))) /\ (meet (rng (f9 | (E /\ E9)))) by A17, A73, XBOOLE_1:16 ;

hence meet (rng g) = (meet (rng f)) /\ (meet (rng f9)) by A92, A99, A97, A100, A98, SETFAM_1:9; :: thesis: verum

suppose A101:
not E9 \ E = {}
; :: thesis: meet (rng g) = (meet (rng f)) /\ (meet (rng f9))

( E9 \ E c= E9 & E9 c= E \/ E9 )
by XBOOLE_1:7, XBOOLE_1:36;

then E9 \ E c= dom g by A8;

then meet (rng g) = (meet ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9))))) /\ (meet (rng (g | (E9 \ E)))) by A8, A63, A81, A94, A101, SETFAM_1:9

.= ((meet (rng (g | (E /\ E9)))) /\ (meet (rng (g | (E \ E9))))) /\ (meet (rng (g | (E9 \ E)))) by A8, A81, A94, A93, SETFAM_1:9 ;

then A102: meet (rng g) = (((meet (rng (f | (E /\ E9)))) /\ (meet (rng (f | (E \ E9))))) /\ (meet (rng (f9 | (E /\ E9))))) /\ (meet (rng (f9 | (E9 \ E)))) by A17, A73, A68, XBOOLE_1:16;

E /\ E9 c= E by XBOOLE_1:17;

then A103: E /\ E9 c= dom f by FUNCT_2:def 1;

E \/ (E /\ E9) = E by XBOOLE_1:12, XBOOLE_1:17;

then dom f = E \/ (E /\ E9) by FUNCT_2:def 1;

then A104: rng f = ((rng (f | (E /\ (E /\ E9)))) \/ (rng (f | (E \ (E /\ E9))))) \/ (rng (f | ((E /\ E9) \ E))) by A49;

E /\ E9 c= E by XBOOLE_1:17;

then (E /\ E9) \ E = {} by XBOOLE_1:37;

then A105: rng (f | ((E /\ E9) \ E)) = {} ;

E9 \ E c= E9 by XBOOLE_1:36;

then A106: E9 \ E c= dom f9 by FUNCT_2:def 1;

E /\ E9 c= E9 by XBOOLE_1:17;

then A107: E /\ E9 c= dom f9 by FUNCT_2:def 1;

E /\ E9 c= E9 by XBOOLE_1:17;

then A108: ( E9 \ E = E9 \ (E /\ E9) & (E /\ E9) \ E9 = {} ) by XBOOLE_1:37, XBOOLE_1:47;

E9 \/ (E /\ E9) = E9 by XBOOLE_1:12, XBOOLE_1:17;

then A109: dom f9 = E9 \/ (E /\ E9) by FUNCT_2:def 1;

E9 /\ (E /\ E9) = (E9 /\ E9) /\ E by XBOOLE_1:16

.= E /\ E9 ;

then rng f9 = ((rng (f9 | (E /\ E9))) \/ (rng (f9 | (E9 \ E)))) \/ (rng (f9 | {})) by A49, A109, A108;

then A110: meet (rng f9) = (meet (rng (f9 | (E /\ E9)))) /\ (meet (rng (f9 | (E9 \ E)))) by A81, A101, A107, A106, SETFAM_1:9;

E \ E9 c= E by XBOOLE_1:36;

then A111: E \ E9 c= dom f by FUNCT_2:def 1;

E /\ (E /\ E9) = (E /\ E) /\ E9 by XBOOLE_1:16

.= E /\ E9 ;

then rng f = (rng (f | (E /\ E9))) \/ (rng (f | (E \ E9))) by A104, A105, XBOOLE_1:47;

then meet (rng f) = (meet (rng (f | (E /\ E9)))) /\ (meet (rng (f | (E \ E9)))) by A81, A92, A103, A111, SETFAM_1:9;

hence meet (rng g) = (meet (rng f)) /\ (meet (rng f9)) by A110, A102, XBOOLE_1:16; :: thesis: verum

end;then E9 \ E c= dom g by A8;

then meet (rng g) = (meet ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9))))) /\ (meet (rng (g | (E9 \ E)))) by A8, A63, A81, A94, A101, SETFAM_1:9

.= ((meet (rng (g | (E /\ E9)))) /\ (meet (rng (g | (E \ E9))))) /\ (meet (rng (g | (E9 \ E)))) by A8, A81, A94, A93, SETFAM_1:9 ;

then A102: meet (rng g) = (((meet (rng (f | (E /\ E9)))) /\ (meet (rng (f | (E \ E9))))) /\ (meet (rng (f9 | (E /\ E9))))) /\ (meet (rng (f9 | (E9 \ E)))) by A17, A73, A68, XBOOLE_1:16;

E /\ E9 c= E by XBOOLE_1:17;

then A103: E /\ E9 c= dom f by FUNCT_2:def 1;

E \/ (E /\ E9) = E by XBOOLE_1:12, XBOOLE_1:17;

then dom f = E \/ (E /\ E9) by FUNCT_2:def 1;

then A104: rng f = ((rng (f | (E /\ (E /\ E9)))) \/ (rng (f | (E \ (E /\ E9))))) \/ (rng (f | ((E /\ E9) \ E))) by A49;

E /\ E9 c= E by XBOOLE_1:17;

then (E /\ E9) \ E = {} by XBOOLE_1:37;

then A105: rng (f | ((E /\ E9) \ E)) = {} ;

E9 \ E c= E9 by XBOOLE_1:36;

then A106: E9 \ E c= dom f9 by FUNCT_2:def 1;

E /\ E9 c= E9 by XBOOLE_1:17;

then A107: E /\ E9 c= dom f9 by FUNCT_2:def 1;

E /\ E9 c= E9 by XBOOLE_1:17;

then A108: ( E9 \ E = E9 \ (E /\ E9) & (E /\ E9) \ E9 = {} ) by XBOOLE_1:37, XBOOLE_1:47;

E9 \/ (E /\ E9) = E9 by XBOOLE_1:12, XBOOLE_1:17;

then A109: dom f9 = E9 \/ (E /\ E9) by FUNCT_2:def 1;

E9 /\ (E /\ E9) = (E9 /\ E9) /\ E by XBOOLE_1:16

.= E /\ E9 ;

then rng f9 = ((rng (f9 | (E /\ E9))) \/ (rng (f9 | (E9 \ E)))) \/ (rng (f9 | {})) by A49, A109, A108;

then A110: meet (rng f9) = (meet (rng (f9 | (E /\ E9)))) /\ (meet (rng (f9 | (E9 \ E)))) by A81, A101, A107, A106, SETFAM_1:9;

E \ E9 c= E by XBOOLE_1:36;

then A111: E \ E9 c= dom f by FUNCT_2:def 1;

E /\ (E /\ E9) = (E /\ E) /\ E9 by XBOOLE_1:16

.= E /\ E9 ;

then rng f = (rng (f | (E /\ E9))) \/ (rng (f | (E \ E9))) by A104, A105, XBOOLE_1:47;

then meet (rng f) = (meet (rng (f | (E /\ E9)))) /\ (meet (rng (f | (E \ E9)))) by A81, A92, A103, A111, SETFAM_1:9;

hence meet (rng g) = (meet (rng f)) /\ (meet (rng f9)) by A110, A102, XBOOLE_1:16; :: thesis: verum

y in Omega

proof

then reconsider xX = x /\ X as Subset of Omega by A4, A6, TARSKI:def 3;
let y be object ; :: thesis: ( y in (meet (rng f)) /\ (meet (rng f9)) implies y in Omega )

consider S being object such that

A112: S in rng f by XBOOLE_0:def 1;

consider S9 being object such that

A113: S9 in rng f9 by XBOOLE_0:def 1;

assume A114: y in (meet (rng f)) /\ (meet (rng f9)) ; :: thesis: y in Omega

reconsider S = S, S9 = S9 as set by TARSKI:1;

y in meet (rng f9) by XBOOLE_0:def 4, A114;

then A115: y in S9 by A113, SETFAM_1:def 1;

y in meet (rng f) by A114, XBOOLE_0:def 4;

then y in S by A112, SETFAM_1:def 1;

then A116: y in S /\ S9 by A115, XBOOLE_0:def 4;

S /\ S9 is Event of Sigma by A112, A113, PROB_1:19;

hence y in Omega by A116; :: thesis: verum

end;consider S being object such that

A112: S in rng f by XBOOLE_0:def 1;

consider S9 being object such that

A113: S9 in rng f9 by XBOOLE_0:def 1;

assume A114: y in (meet (rng f)) /\ (meet (rng f9)) ; :: thesis: y in Omega

reconsider S = S, S9 = S9 as set by TARSKI:1;

y in meet (rng f9) by XBOOLE_0:def 4, A114;

then A115: y in S9 by A113, SETFAM_1:def 1;

y in meet (rng f) by A114, XBOOLE_0:def 4;

then y in S by A112, SETFAM_1:def 1;

then A116: y in S /\ S9 by A115, XBOOLE_0:def 4;

S /\ S9 is Event of Sigma by A112, A113, PROB_1:19;

hence y in Omega by A116; :: thesis: verum

E \/ E9 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