let X be non empty set ; :: thesis: for S being SigmaField of X

for f being with_the_same_dom Functional_Sequence of X,REAL

for F being SetSequence of S

for r being Real st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),r)) ) holds

meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),r))

let S be SigmaField of X; :: thesis: for f being with_the_same_dom Functional_Sequence of X,REAL

for F being SetSequence of S

for r being Real st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),r)) ) holds

meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),r))

let f be with_the_same_dom Functional_Sequence of X,REAL; :: thesis: for F being SetSequence of S

for r being Real st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),r)) ) holds

meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),r))

let F be SetSequence of S; :: thesis: for r being Real st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),r)) ) holds

meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),r))

let r be Real; :: thesis: ( ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),r)) ) implies meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),r)) )

set E = dom (f . 0);

assume A1: for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),r)) ; :: thesis: meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),r))

hence meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),r)) by A8; :: thesis: verum

for f being with_the_same_dom Functional_Sequence of X,REAL

for F being SetSequence of S

for r being Real st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),r)) ) holds

meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),r))

let S be SigmaField of X; :: thesis: for f being with_the_same_dom Functional_Sequence of X,REAL

for F being SetSequence of S

for r being Real st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),r)) ) holds

meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),r))

let f be with_the_same_dom Functional_Sequence of X,REAL; :: thesis: for F being SetSequence of S

for r being Real st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),r)) ) holds

meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),r))

let F be SetSequence of S; :: thesis: for r being Real st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),r)) ) holds

meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),r))

let r be Real; :: thesis: ( ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),r)) ) implies meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),r)) )

set E = dom (f . 0);

assume A1: for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),r)) ; :: thesis: meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),r))

now :: thesis: for x being object st x in meet (rng F) holds

x in (dom (f . 0)) /\ (great_eq_dom ((inf f),r))

then A8:
meet (rng F) c= (dom (f . 0)) /\ (great_eq_dom ((inf f),r))
;x in (dom (f . 0)) /\ (great_eq_dom ((inf f),r))

let x be object ; :: thesis: ( x in meet (rng F) implies x in (dom (f . 0)) /\ (great_eq_dom ((inf f),r)) )

assume A2: x in meet (rng F) ; :: thesis: x in (dom (f . 0)) /\ (great_eq_dom ((inf f),r))

then reconsider z = x as Element of X ;

A3: F . 0 = (dom (f . 0)) /\ (great_eq_dom ((f . 0),r)) by A1;

F . 0 in rng F by FUNCT_2:4;

then x in F . 0 by A2, SETFAM_1:def 1;

then A4: x in dom (f . 0) by A3, XBOOLE_0:def 4;

then A5: x in dom (inf f) by MESFUNC8:def 3;

r <= p

then r <= inf (rng (R_EAL (f # z))) by XXREAL_2:def 4;

then r <= (inf f) . x by A5, Th2;

then x in great_eq_dom ((inf f),r) by A5, MESFUNC1:def 14;

hence x in (dom (f . 0)) /\ (great_eq_dom ((inf f),r)) by A4, XBOOLE_0:def 4; :: thesis: verum

end;assume A2: x in meet (rng F) ; :: thesis: x in (dom (f . 0)) /\ (great_eq_dom ((inf f),r))

then reconsider z = x as Element of X ;

A3: F . 0 = (dom (f . 0)) /\ (great_eq_dom ((f . 0),r)) by A1;

F . 0 in rng F by FUNCT_2:4;

then x in F . 0 by A2, SETFAM_1:def 1;

then A4: x in dom (f . 0) by A3, XBOOLE_0:def 4;

then A5: x in dom (inf f) by MESFUNC8:def 3;

A6: now :: thesis: for n being Element of NAT holds r <= (R_EAL (f # z)) . n

for p being ExtReal st p in rng (R_EAL (f # z)) holds let n be Element of NAT ; :: thesis: r <= (R_EAL (f # z)) . n

F . n in rng F by FUNCT_2:4;

then A7: z in F . n by A2, SETFAM_1:def 1;

F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),r)) by A1;

then x in great_eq_dom ((f . n),r) by A7, XBOOLE_0:def 4;

then r <= (f . n) . z by MESFUNC1:def 14;

hence r <= (R_EAL (f # z)) . n by SEQFUNC:def 10; :: thesis: verum

end;F . n in rng F by FUNCT_2:4;

then A7: z in F . n by A2, SETFAM_1:def 1;

F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),r)) by A1;

then x in great_eq_dom ((f . n),r) by A7, XBOOLE_0:def 4;

then r <= (f . n) . z by MESFUNC1:def 14;

hence r <= (R_EAL (f # z)) . n by SEQFUNC:def 10; :: thesis: verum

r <= p

proof

then
r is LowerBound of rng (R_EAL (f # z))
by XXREAL_2:def 2;
let p be ExtReal; :: thesis: ( p in rng (R_EAL (f # z)) implies r <= p )

assume p in rng (R_EAL (f # z)) ; :: thesis: r <= p

then ex n being object st

( n in NAT & (R_EAL (f # z)) . n = p ) by FUNCT_2:11;

hence r <= p by A6; :: thesis: verum

end;assume p in rng (R_EAL (f # z)) ; :: thesis: r <= p

then ex n being object st

( n in NAT & (R_EAL (f # z)) . n = p ) by FUNCT_2:11;

hence r <= p by A6; :: thesis: verum

then r <= inf (rng (R_EAL (f # z))) by XXREAL_2:def 4;

then r <= (inf f) . x by A5, Th2;

then x in great_eq_dom ((inf f),r) by A5, MESFUNC1:def 14;

hence x in (dom (f . 0)) /\ (great_eq_dom ((inf f),r)) by A4, XBOOLE_0:def 4; :: thesis: verum

now :: thesis: for x being object st x in (dom (f . 0)) /\ (great_eq_dom ((inf f),r)) holds

x in meet (rng F)

then
(dom (f . 0)) /\ (great_eq_dom ((inf f),r)) c= meet (rng F)
;x in meet (rng F)

let x be object ; :: thesis: ( x in (dom (f . 0)) /\ (great_eq_dom ((inf f),r)) implies x in meet (rng F) )

assume A9: x in (dom (f . 0)) /\ (great_eq_dom ((inf f),r)) ; :: thesis: x in meet (rng F)

then reconsider z = x as Element of X ;

A10: x in dom (f . 0) by A9, XBOOLE_0:def 4;

x in great_eq_dom ((inf f),r) by A9, XBOOLE_0:def 4;

then A11: r <= (inf f) . z by MESFUNC1:def 14;

end;assume A9: x in (dom (f . 0)) /\ (great_eq_dom ((inf f),r)) ; :: thesis: x in meet (rng F)

then reconsider z = x as Element of X ;

A10: x in dom (f . 0) by A9, XBOOLE_0:def 4;

x in great_eq_dom ((inf f),r) by A9, XBOOLE_0:def 4;

then A11: r <= (inf f) . z by MESFUNC1:def 14;

now :: thesis: for y being set st y in rng F holds

x in y

hence
x in meet (rng F)
by SETFAM_1:def 1; :: thesis: verumx in y

let y be set ; :: thesis: ( y in rng F implies x in y )

assume y in rng F ; :: thesis: x in y

then consider n being object such that

A12: n in NAT and

A13: y = F . n by FUNCT_2:11;

reconsider n = n as Element of NAT by A12;

A14: x in dom (f . n) by A10, MESFUNC8:def 2;

x in dom (inf f) by A10, MESFUNC8:def 3;

then A15: (inf f) . z = inf (rng (R_EAL (f # z))) by Th2;

(f . n) . z = (R_EAL (f # z)) . n by SEQFUNC:def 10;

then (f . n) . z >= inf (rng (R_EAL (f # z))) by FUNCT_2:4, XXREAL_2:3;

then r <= (f . n) . z by A11, A15, XXREAL_0:2;

then A16: x in great_eq_dom ((f . n),r) by A14, MESFUNC1:def 14;

F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),r)) by A1;

hence x in y by A10, A13, A16, XBOOLE_0:def 4; :: thesis: verum

end;assume y in rng F ; :: thesis: x in y

then consider n being object such that

A12: n in NAT and

A13: y = F . n by FUNCT_2:11;

reconsider n = n as Element of NAT by A12;

A14: x in dom (f . n) by A10, MESFUNC8:def 2;

x in dom (inf f) by A10, MESFUNC8:def 3;

then A15: (inf f) . z = inf (rng (R_EAL (f # z))) by Th2;

(f . n) . z = (R_EAL (f # z)) . n by SEQFUNC:def 10;

then (f . n) . z >= inf (rng (R_EAL (f # z))) by FUNCT_2:4, XXREAL_2:3;

then r <= (f . n) . z by A11, A15, XXREAL_0:2;

then A16: x in great_eq_dom ((f . n),r) by A14, MESFUNC1:def 14;

F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),r)) by A1;

hence x in y by A10, A13, A16, XBOOLE_0:def 4; :: thesis: verum

hence meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),r)) by A8; :: thesis: verum