let X be set ; :: thesis: for S being SigmaField of X
for F being Function of NAT ,S
for f being PartFunc of X, ExtREAL
for A being set st ( for n being Element of NAT holds F . n = A /\ (less_dom f,(R_EAL (- n))) ) holds
A /\ (eq_dom f,-infty ) = meet (rng F)
let S be SigmaField of X; :: thesis: for F being Function of NAT ,S
for f being PartFunc of X, ExtREAL
for A being set st ( for n being Element of NAT holds F . n = A /\ (less_dom f,(R_EAL (- n))) ) holds
A /\ (eq_dom f,-infty ) = meet (rng F)
let F be Function of NAT ,S; :: thesis: for f being PartFunc of X, ExtREAL
for A being set st ( for n being Element of NAT holds F . n = A /\ (less_dom f,(R_EAL (- n))) ) holds
A /\ (eq_dom f,-infty ) = meet (rng F)
let f be PartFunc of X, ExtREAL ; :: thesis: for A being set st ( for n being Element of NAT holds F . n = A /\ (less_dom f,(R_EAL (- n))) ) holds
A /\ (eq_dom f,-infty ) = meet (rng F)
let A be set ; :: thesis: ( ( for n being Element of NAT holds F . n = A /\ (less_dom f,(R_EAL (- n))) ) implies A /\ (eq_dom f,-infty ) = meet (rng F) )
assume A1: for n being Element of NAT holds F . n = A /\ (less_dom f,(R_EAL (- n))) ; :: thesis: A /\ (eq_dom f,-infty ) = meet (rng F)
A2: A /\ (eq_dom f,-infty ) c= meet (rng F)

proof

for x being set st x in A /\ (eq_dom f,-infty ) holds
x in meet (rng F)

proof

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

proof

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

proof

assume Y in rng F ; :: thesis: x in Y
then consider m being Element of NAT such that
A5: ( m in dom F & Y = F . m ) by PARTFUN1:26;
A6: Y = A /\ (less_dom f,(R_EAL (- m))) by A1, A5;
A7: x in dom f by A4, Def16;
reconsider x = x as Element of X by A3;
A8: f . x = -infty by A4, Def16;
not R_EAL (- m) <= -infty by XXREAL_0:12;
then x in less_dom f,(R_EAL (- m)) by A7, A8, Def12;
hence x in Y by A4, A6, XBOOLE_0:def 4; :: thesis: verum

end;

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

end;

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

end;

hence A /\ (eq_dom f,-infty ) c= meet (rng F) by TARSKI:def 3; :: thesis: verum

end;

meet (rng F) c= A /\ (eq_dom f,-infty )

proof

for x being set st x in meet (rng F) holds
x in A /\ (eq_dom f,-infty )

proof

let x be set ; :: thesis: ( x in meet (rng F) implies x in A /\ (eq_dom f,-infty ) )
assume A9: x in meet (rng F) ; :: thesis: x in A /\ (eq_dom f,-infty )
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 ) )

proof

let m be Element of NAT ; :: thesis: ( x in A & x in dom f & ex y being R_eal st
( y = f . x & y = -infty ) )
m in NAT ;
then m in dom F by FUNCT_2:def 1;
then F . m in rng F by FUNCT_1:def 5;
then x in F . m by A9, SETFAM_1:def 1;
then x in A /\ (less_dom f,(R_EAL (- m))) by A1;
then A11: ( x in A & x in less_dom f,(R_EAL (- m)) ) by XBOOLE_0:def 4;
for r being Real holds f . x < R_EAL r

proof

let r be Real; :: thesis: f . x < R_EAL r
consider n being Element of NAT such that
A12: - n <= r by Th12;
n in NAT ;
then n in dom F by FUNCT_2:def 1;
then F . n in rng F by FUNCT_1:def 5;
then x in F . n by A9, SETFAM_1:def 1;
then x in A /\ (less_dom f,(R_EAL (- n))) by A1;
then x in less_dom f,(R_EAL (- n)) by XBOOLE_0:def 4;
then f . x < R_EAL (- n) by Def12;
hence f . x < R_EAL r by A12, XXREAL_0:2; :: thesis: verum

end;

then f . x = -infty by Th16;
hence ( x in A & x in dom f & ex y being R_eal st
( y = f . x & y = -infty ) ) by A11, Def12; :: thesis: verum

end;

1 in NAT ;
then 1 in dom F by FUNCT_2:def 1;
then F . 1 in rng F by FUNCT_1:def 5;
then x in F . 1 by A9, SETFAM_1:def 1;
then x in A /\ (less_dom f,(R_EAL (- 1))) by A1;
then reconsider x = x as Element of X ;
x in eq_dom f,-infty by A10, Def16;
hence x in A /\ (eq_dom f,-infty ) by A10, XBOOLE_0:def 4; :: thesis: verum

end;

hence meet (rng F) c= A /\ (eq_dom f,-infty ) by TARSKI:def 3; :: thesis: verum

end;

hence A /\ (eq_dom f,-infty ) = meet (rng F) by A2, XBOOLE_0:def 10; :: thesis: verum