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: 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)
A5: x in A by A4, XBOOLE_0:def 4;
A6: x in less_dom f,(R_EAL r) by A4, XBOOLE_0:def 4;
A7: ex Y being set st
( x in Y & Y in rng F )

proof

reconsider x = x as Element of X by A4;
A8: x in dom f by A6, Def12;
A9: f . x < R_EAL r by A6, Def12;
A10: 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 A11: 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 A11, XXREAL_0:5; :: thesis: verum

end;

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

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

end;

end;

end;

consider m being Element of NAT such that
A17: f . x <= R_EAL (r - (1 / (m + 1))) by A10;
A18: x in less_eq_dom f,(R_EAL (r - (1 / (m + 1)))) by A8, A17, Def13;
A19: x in A /\ (less_eq_dom f,(R_EAL (r - (1 / (m + 1))))) by A5, A18, XBOOLE_0:def 4;
A20: m in NAT ;
A21: m in dom F by A20, 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, A19, A21, FUNCT_1:def 5; :: thesis: verum

end;

thus x in union (rng F) by A7, TARSKI:def 4; :: thesis: verum

end;

A22: A /\ (less_dom f,(R_EAL r)) c= union (rng F) by A3, TARSKI:def 3;
A23: 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 A24: x in union (rng F) ; :: thesis: x in A /\ (less_dom f,(R_EAL r))
consider Y being set such that
A25: x in Y and
A26: Y in rng F by A24, TARSKI:def 4;
consider m being Element of NAT such that
m in dom F and
A27: F . m = Y by A26, PARTFUN1:26;
A28: x in A /\ (less_eq_dom f,(R_EAL (r - (1 / (m + 1))))) by A2, A25, A27;
A29: x in A by A28, XBOOLE_0:def 4;
A30: x in less_eq_dom f,(R_EAL (r - (1 / (m + 1)))) by A28, XBOOLE_0:def 4;
A31: x in dom f by A30, Def13;
A32: f . x <= R_EAL (r - (1 / (m + 1))) by A30, Def13;
reconsider x = x as Element of X by A25, A26;
A33: f . x < R_EAL r

proof

A34: now

A36: r < r + (1 / (m + 1)) by XREAL_1:31, XREAL_1:141;
A37: r - (1 / (m + 1)) < r by A36, XREAL_1:21;
thus f . x < R_EAL r by A32, A37, XXREAL_0:2; :: thesis: verum

end;

thus f . x < R_EAL r by A34; :: thesis: verum

end;

A38: x in less_dom f,(R_EAL r) by A31, A33, Def12;
thus x in A /\ (less_dom f,(R_EAL r)) by A29, A38, XBOOLE_0:def 4; :: thesis: verum

end;

A39: union (rng F) c= A /\ (less_dom f,(R_EAL r)) by A23, TARSKI:def 3;
thus A /\ (less_dom f,(R_EAL r)) = union (rng F) by A22, A39, XBOOLE_0:def 10; :: thesis: verum