let X be set ; :: thesis:
let S be SigmaField of X; :: thesis:
let F be sequence of S; :: thesis:
let f be PartFunc of X,ExtREAL; :: thesis:
let A be set ; :: thesis:
assume A1: for n being Element of NAT holds F . n = A /\ (great_dom (f,n)) ; :: thesis:
for x being object st x in A /\ (eq_dom (f,+infty)) holds
x in meet (rng F)

let x be object ; :: thesis:
assume A2: x in A /\ (eq_dom (f,+infty)) ; :: thesis:
then A3: x in A by XBOOLE_0:def 4;
A4: x in eq_dom (f,+infty) by A2, XBOOLE_0:def 4;
for Y being set st Y in rng F holds
x in Y

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

assume Y in rng F ; :: thesis:
then consider m being Element of NAT such that
m in dom F and
A5: Y = F . m by PARTFUN1:3;
A6: Y = A /\ (great_dom (f,m)) by A1, A5;
reconsider x = x as Element of X by A2;
A7: f . x = +infty by A4, Def15;
m in REAL by XREAL_0:def 1;
then ( x in dom f & not +infty <= m ) by A4, Def15, XXREAL_0:9;
then x in great_dom (f,m) by A7, Def13;
hence x in Y by A3, A6, XBOOLE_0:def 4; :: thesis:

end;

hence ( Y in rng F implies x in Y ) ; :: thesis:

end;

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

end;

then A8: A /\ (eq_dom (f,+infty)) c= meet (rng F) ;
for x being object st x in meet (rng F) holds
x in A /\ (eq_dom (f,+infty))

let x be object ; :: thesis:
reconsider xx = x as set by TARSKI:1;
assume A9: x in meet (rng F) ; :: thesis:
A10: for m being Element of NAT holds
( x in A & x in dom f & ex y being R_eal st
( y = f . x & y = +infty ) )

let m be Element of NAT ; :: thesis:
m in NAT ;
then m in dom F by FUNCT_2:def 1;
then F . m in rng F by FUNCT_1:def 3;
then x in F . m by A9, SETFAM_1:def 1;
then A11: x in A /\ (great_dom (f,m)) by A1;
then A12: x in great_dom (f,m) by XBOOLE_0:def 4;
for r being Real holds r < f . xx

let r be Real; :: thesis:
consider n being Element of NAT such that
A13: r <= n by Th8;
n in NAT ;
then n in dom F by FUNCT_2:def 1;
then F . n in rng F by FUNCT_1:def 3;
then x in F . n by A9, SETFAM_1:def 1;
then x in A /\ (great_dom (f,n)) by A1;
then x in great_dom (f,n) by XBOOLE_0:def 4;
then n < f . x by Def13;
hence r < f . xx by A13, XXREAL_0:2; :: thesis:

end;

then f . x = +infty by Th12;
hence ( x in A & x in dom f & ex y being R_eal st
( y = f . x & y = +infty ) ) by A11, A12, Def13, XBOOLE_0:def 4; :: thesis:

end;

1 in NAT ;
then 1 in dom F by FUNCT_2:def 1;
then F . 1 in rng F by FUNCT_1:def 3;
then x in F . 1 by A9, SETFAM_1:def 1;
then x in A /\ (great_dom (f,1)) by A1;
then reconsider x = x as Element of X ;
x in eq_dom (f,+infty) by A10, Def15;
hence x in A /\ (eq_dom (f,+infty)) by A10, XBOOLE_0:def 4; :: thesis:

end;

then meet (rng F) c= A /\ (eq_dom (f,+infty)) ;
hence A /\ (eq_dom (f,+infty)) = meet (rng F) by A8, XBOOLE_0:def 10; :: thesis: