let X be set ; :: thesis: for f being PartFunc of X,ExtREAL
for S being SigmaField of X
for F being Function of NAT ,S
for A being set
for r being real number st ( for n being Element of NAT holds F . n = A /\ (less_eq_dom f,(R_EAL (r - (1 / (n + 1))))) ) holds
A /\ (less_dom f,(R_EAL r)) = union (rng F)
let f be PartFunc of X,ExtREAL ; :: thesis: for S being SigmaField of X
for F being Function of NAT ,S
for A being set
for r being real number st ( for n being Element of NAT holds F . n = A /\ (less_eq_dom f,(R_EAL (r - (1 / (n + 1))))) ) holds
A /\ (less_dom f,(R_EAL r)) = union (rng F)
let S be SigmaField of X; :: thesis: for F being Function of NAT ,S
for A being set
for r being real number st ( for n being Element of NAT holds F . n = A /\ (less_eq_dom f,(R_EAL (r - (1 / (n + 1))))) ) holds
A /\ (less_dom f,(R_EAL r)) = union (rng F)
let F be Function of NAT ,S; :: thesis: for A being set
for r being real number st ( for n being Element of NAT holds F . n = A /\ (less_eq_dom f,(R_EAL (r - (1 / (n + 1))))) ) holds
A /\ (less_dom f,(R_EAL r)) = union (rng F)
let A be set ; :: thesis: for r being real number st ( for n being Element of NAT holds F . n = A /\ (less_eq_dom f,(R_EAL (r - (1 / (n + 1))))) ) holds
A /\ (less_dom f,(R_EAL r)) = union (rng F)
let r be real number ; :: thesis: ( ( for n being Element of NAT holds F . n = A /\ (less_eq_dom f,(R_EAL (r - (1 / (n + 1))))) ) implies A /\ (less_dom f,(R_EAL r)) = union (rng F) )
A1: r in REAL by XREAL_0:def 1;
assume A2: for n being Element of NAT holds F . n = A /\ (less_eq_dom f,(R_EAL (r - (1 / (n + 1))))) ; :: thesis: A /\ (less_dom f,(R_EAL r)) = union (rng F)
A3: A /\ (less_dom f,(R_EAL r)) c= union (rng F)

proof

for x being set st x in A /\ (less_dom f,(R_EAL r)) holds
x in union (rng F)

proof

let x be set ; :: thesis: ( x in A /\ (less_dom f,(R_EAL r)) implies x in union (rng F) )
assume A4: x in A /\ (less_dom f,(R_EAL r)) ; :: thesis: x in union (rng F)
then A5: ( x in A & x in less_dom f,(R_EAL r) ) by XBOOLE_0:def 4;
ex Y being set st
( x in Y & Y in rng F )

proof

reconsider x = x as Element of X by A4;
A6: x in dom f by A5, Def12;
A7: f . x < R_EAL r by A5, Def12;
ex m being Element of NAT st f . x <= R_EAL (r - (1 / (m + 1)))

proof

per cases ( f . x = -infty or not f . x = -infty ) ;

suppose A8: f . x = -infty ; :: thesis: ex m being Element of NAT st f . x <= R_EAL (r - (1 / (m + 1)))

take 1 ; :: thesis: f . x <= R_EAL (r - (1 / (1 + 1)))
thus f . x <= R_EAL (r - (1 / (1 + 1))) by A8, XXREAL_0:5; :: thesis: verum

end;

suppose not f . x = -infty ; :: thesis: ex m being Element of NAT st f . x <= R_EAL (r - (1 / (m + 1)))

then not f . x <= -infty by XXREAL_0:6;
then reconsider y1 = f . x as Real by A7, XXREAL_0:48;
consider m being Element of NAT such that
A9: 1 / (m + 1) < r - y1 by A7, Th13;
y1 + (1 / (m + 1)) < r by A9, XREAL_1:22;
then f . x <= R_EAL (r - (1 / (m + 1))) by XREAL_1:22;
hence ex m being Element of NAT st f . x <= R_EAL (r - (1 / (m + 1))) ; :: thesis: verum

end;

end;

end;

then consider m being Element of NAT such that
A10: f . x <= R_EAL (r - (1 / (m + 1))) ;
x in less_eq_dom f,(R_EAL (r - (1 / (m + 1)))) by A6, A10, Def13;
then A11: x in A /\ (less_eq_dom f,(R_EAL (r - (1 / (m + 1))))) by A5, XBOOLE_0:def 4;
m in NAT ;
then A12: m in dom F by FUNCT_2:def 1;
take F . m ; :: thesis: ( x in F . m & F . m in rng F )
thus ( x in F . m & F . m in rng F ) by A2, A11, A12, FUNCT_1:def 5; :: thesis: verum

end;

hence x in union (rng F) by TARSKI:def 4; :: thesis: verum

end;

hence A /\ (less_dom f,(R_EAL r)) c= union (rng F) by TARSKI:def 3; :: thesis: verum

end;

union (rng F) c= A /\ (less_dom f,(R_EAL r))

proof

for x being set st x in union (rng F) holds
x in A /\ (less_dom f,(R_EAL r))

proof

let x be set ; :: thesis: ( x in union (rng F) implies x in A /\ (less_dom f,(R_EAL r)) )
assume x in union (rng F) ; :: thesis: x in A /\ (less_dom f,(R_EAL r))
then consider Y being set such that
A13: ( x in Y & Y in rng F ) by TARSKI:def 4;
consider m being Element of NAT such that
A14: ( m in dom F & F . m = Y ) by A13, PARTFUN1:26;
x in A /\ (less_eq_dom f,(R_EAL (r - (1 / (m + 1))))) by A2, A13, A14;
then A15: ( x in A & x in less_eq_dom f,(R_EAL (r - (1 / (m + 1)))) ) by XBOOLE_0:def 4;
then A16: x in dom f by Def13;
A17: f . x <= R_EAL (r - (1 / (m + 1))) by A15, Def13;
reconsider x = x as Element of X by A13;
f . x < R_EAL r

proof

now

per cases ( f . x = -infty or not f . x = -infty ) ;

suppose f . x = -infty ; :: thesis: f . x < R_EAL r

hence f . x < R_EAL r by A1, XXREAL_0:12; :: thesis: verum

end;

suppose not f . x = -infty ; :: thesis: f . x < R_EAL r

1 / (m + 1) > 0 by XREAL_1:141;
then r < r + (1 / (m + 1)) by XREAL_1:31;
then r - (1 / (m + 1)) < r by XREAL_1:21;
hence f . x < R_EAL r by A17, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence f . x < R_EAL r ; :: thesis: verum

end;

then x in less_dom f,(R_EAL r) by A16, Def12;
hence x in A /\ (less_dom f,(R_EAL r)) by A15, XBOOLE_0:def 4; :: thesis: verum

end;

hence union (rng F) c= A /\ (less_dom f,(R_EAL r)) by TARSKI:def 3; :: thesis: verum

end;

hence A /\ (less_dom f,(R_EAL r)) = union (rng F) by A3, XBOOLE_0:def 10; :: thesis: verum