let X be non empty set ; :: thesis: for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for F being SetSequence of S
for r being real number st ( for n being natural number holds F . n = (dom (f . 0 )) /\ (great_eq_dom (f . n),(R_EAL r)) ) holds
meet (rng F) = (dom (f . 0 )) /\ (great_eq_dom (inf f),(R_EAL r))
let S be SigmaField of X; :: thesis: for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for F being SetSequence of S
for r being real number st ( for n being natural number holds F . n = (dom (f . 0 )) /\ (great_eq_dom (f . n),(R_EAL r)) ) holds
meet (rng F) = (dom (f . 0 )) /\ (great_eq_dom (inf f),(R_EAL r))
let f be with_the_same_dom Functional_Sequence of X,ExtREAL ; :: thesis: for F being SetSequence of S
for r being real number st ( for n being natural number holds F . n = (dom (f . 0 )) /\ (great_eq_dom (f . n),(R_EAL r)) ) holds
meet (rng F) = (dom (f . 0 )) /\ (great_eq_dom (inf f),(R_EAL r))
let F be SetSequence of S; :: thesis: for r being real number st ( for n being natural number holds F . n = (dom (f . 0 )) /\ (great_eq_dom (f . n),(R_EAL r)) ) holds
meet (rng F) = (dom (f . 0 )) /\ (great_eq_dom (inf f),(R_EAL r))
let r be real number ; :: thesis: ( ( for n being natural number holds F . n = (dom (f . 0 )) /\ (great_eq_dom (f . n),(R_EAL r)) ) implies meet (rng F) = (dom (f . 0 )) /\ (great_eq_dom (inf f),(R_EAL r)) )
set E = dom (f . 0 );
assume A1: for n being natural number holds F . n = (dom (f . 0 )) /\ (great_eq_dom (f . n),(R_EAL r)) ; :: thesis: meet (rng F) = (dom (f . 0 )) /\ (great_eq_dom (inf f),(R_EAL r))

now

let x be set ; :: thesis: ( x in meet (rng F) implies x in (dom (f . 0 )) /\ (great_eq_dom (inf f),(R_EAL r)) )
assume A2: x in meet (rng F) ; :: thesis: x in (dom (f . 0 )) /\ (great_eq_dom (inf f),(R_EAL r))
then reconsider z = x as Element of X ;
A3: F . 0 = (dom (f . 0 )) /\ (great_eq_dom (f . 0 ),(R_EAL r)) by A1;
F . 0 in rng F by FUNCT_2:6;
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 Def3;

A6: now

let n be Element of NAT ; :: thesis: R_EAL r <= (f # z) . n
F . n in rng F by FUNCT_2:6;
then A7: z in F . n by A2, SETFAM_1:def 1;
F . n = (dom (f . 0 )) /\ (great_eq_dom (f . n),(R_EAL r)) by A1;
then x in great_eq_dom (f . n),(R_EAL r) by A7, XBOOLE_0:def 4;
then R_EAL r <= (f . n) . z by MESFUNC1:def 15;
hence R_EAL r <= (f # z) . n by MESFUNC5:def 13; :: thesis: verum

end;

now

let s be ext-real number ; :: thesis: ( s in rng (f # z) implies R_EAL r <= s )
assume s in rng (f # z) ; :: thesis: R_EAL r <= s
then ex k being set st
( k in NAT & s = (f # z) . k ) by FUNCT_2:17;
hence R_EAL r <= s by A6; :: thesis: verum

end;

then R_EAL r is LowerBound of rng (f # z) by XXREAL_2:def 2;
then R_EAL r <= inf (f # z) by XXREAL_2:def 4;
then R_EAL r <= (inf f) . x by A5, Def3;
then x in great_eq_dom (inf f),(R_EAL r) by A5, MESFUNC1:def 15;
hence x in (dom (f . 0 )) /\ (great_eq_dom (inf f),(R_EAL r)) by A4, XBOOLE_0:def 4; :: thesis: verum

end;

then A8: meet (rng F) c= (dom (f . 0 )) /\ (great_eq_dom (inf f),(R_EAL r)) by TARSKI:def 3;

now

let x be set ; :: thesis: ( x in (dom (f . 0 )) /\ (great_eq_dom (inf f),(R_EAL r)) implies x in meet (rng F) )
assume A9: x in (dom (f . 0 )) /\ (great_eq_dom (inf f),(R_EAL 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_EAL r) by A9, XBOOLE_0:def 4;
then A11: R_EAL r <= (inf f) . z by MESFUNC1:def 15;

now

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 set such that
A12: n in NAT and
A13: y = F . n by FUNCT_2:17;
reconsider n = n as Element of NAT by A12;
A14: x in dom (f . n) by A10, Def2;
x in dom (inf f) by A10, Def3;
then A15: (inf f) . z = inf (f # z) by Def3;
A16: x in dom (f . 0 ) by A9, XBOOLE_0:def 4;
(f . n) . z = (f # z) . n by MESFUNC5:def 13;
then inf (f # z) <= (f . n) . z by RINFSUP2:23;
then R_EAL r <= (f . n) . z by A11, A15, XXREAL_0:2;
then A17: x in great_eq_dom (f . n),(R_EAL r) by A14, MESFUNC1:def 15;
F . n = (dom (f . 0 )) /\ (great_eq_dom (f . n),(R_EAL r)) by A1;
hence x in y by A13, A16, A17, XBOOLE_0:def 4; :: thesis: verum

end;

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

end;

then (dom (f . 0 )) /\ (great_eq_dom (inf f),(R_EAL r)) c= meet (rng F) by TARSKI:def 3;
hence meet (rng F) = (dom (f . 0 )) /\ (great_eq_dom (inf f),(R_EAL r)) by A8, XBOOLE_0:def 10; :: thesis: verum