let X be set ; :: thesis: for f being PartFunc of X,ExtREAL
for S being SigmaField of X
for F being sequence of S
for A being set
for r being Real st ( for n being Element of NAT holds F . n = A /\ (less_eq_dom (f,(r - (1 / (n + 1))))) ) holds
A /\ (less_dom (f,r)) = union (rng F)
let f be PartFunc of X,ExtREAL; :: thesis: for S being SigmaField of X
for F being sequence of S
for A being set
for r being Real st ( for n being Element of NAT holds F . n = A /\ (less_eq_dom (f,(r - (1 / (n + 1))))) ) holds
A /\ (less_dom (f,r)) = union (rng F)
let S be SigmaField of X; :: thesis: for F being sequence of S
for A being set
for r being Real st ( for n being Element of NAT holds F . n = A /\ (less_eq_dom (f,(r - (1 / (n + 1))))) ) holds
A /\ (less_dom (f,r)) = union (rng F)
let F be sequence of S; :: thesis: for A being set
for r being Real st ( for n being Element of NAT holds F . n = A /\ (less_eq_dom (f,(r - (1 / (n + 1))))) ) holds
A /\ (less_dom (f,r)) = union (rng F)
let A be set ; :: thesis: for r being Real st ( for n being Element of NAT holds F . n = A /\ (less_eq_dom (f,(r - (1 / (n + 1))))) ) holds
A /\ (less_dom (f,r)) = union (rng F)
let r be Real; :: thesis: ( ( for n being Element of NAT holds F . n = A /\ (less_eq_dom (f,(r - (1 / (n + 1))))) ) implies A /\ (less_dom (f,r)) = union (rng F) )
assume A1: for n being Element of NAT holds F . n = A /\ (less_eq_dom (f,(r - (1 / (n + 1))))) ; :: thesis: A /\ (less_dom (f,r)) = union (rng F)
for x being object st x in A /\ (less_dom (f,r)) holds
x in union (rng F)

proof

let x be object ; :: thesis: ( x in A /\ (less_dom (f,r)) implies x in union (rng F) )
assume A2: x in A /\ (less_dom (f,r)) ; :: thesis: x in union (rng F)
then A3: x in A by XBOOLE_0:def 4;
A4: x in less_dom (f,r) by A2, 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 A2;
A5: x in dom f by A4, Def11;
A6: f . x < r by A4, Def11;
ex m being Element of NAT st f . x <= r - (1 / (m + 1))

proof

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

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

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

end;

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

then not f . x <= -infty by XXREAL_0:6;
then reconsider y1 = f . x as Element of REAL by A6, XXREAL_0:48;
consider m being Element of NAT such that
A8: 1 / (m + 1) < r - y1 by A6, Th10;
y1 + (1 / (m + 1)) < r by A8, XREAL_1:20;
then f . x <= r - (1 / (m + 1)) by XREAL_1:20;
hence ex m being Element of NAT st f . x <= r - (1 / (m + 1)) ; :: thesis: verum

end;

end;

end;

then consider m being Element of NAT such that
A9: f . x <= r - (1 / (m + 1)) ;
x in less_eq_dom (f,(r - (1 / (m + 1)))) by A5, A9, Def12;
then A10: x in A /\ (less_eq_dom (f,(r - (1 / (m + 1))))) by A3, XBOOLE_0:def 4;
m in NAT ;
then A11: 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 A1, A10, A11, FUNCT_1:def 3; :: thesis: verum

end;

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

end;

then A12: A /\ (less_dom (f,r)) c= union (rng F) ;
for x being object st x in union (rng F) holds
x in A /\ (less_dom (f,r))

proof

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

proof

now :: thesis: f . x < r

r < r + (1 / (m + 1)) by XREAL_1:29, XREAL_1:139;
then r - (1 / (m + 1)) < r by XREAL_1:19;
hence f . x < r by A20, XXREAL_0:2; :: thesis: verum

end;

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

end;

then x in less_dom (f,r) by A19, Def11;
hence x in A /\ (less_dom (f,r)) by A17, XBOOLE_0:def 4; :: thesis: verum

end;

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