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
for r being Real st ( for n being Element of NAT holds F . n = A /\ (great_eq_dom f,(R_EAL (r + (1 / (n + 1))))) ) holds
A /\ (great_dom f,(R_EAL r)) = union (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
for r being Real st ( for n being Element of NAT holds F . n = A /\ (great_eq_dom f,(R_EAL (r + (1 / (n + 1))))) ) holds
A /\ (great_dom f,(R_EAL r)) = union (rng F)
let F be Function of NAT ,S; :: thesis: for f being PartFunc of X,ExtREAL
for A being set
for r being Real st ( for n being Element of NAT holds F . n = A /\ (great_eq_dom f,(R_EAL (r + (1 / (n + 1))))) ) holds
A /\ (great_dom f,(R_EAL r)) = union (rng F)
let f be PartFunc of X,ExtREAL ; :: thesis: for A being set
for r being Real st ( for n being Element of NAT holds F . n = A /\ (great_eq_dom f,(R_EAL (r + (1 / (n + 1))))) ) holds
A /\ (great_dom f,(R_EAL r)) = union (rng F)
let A be set ; :: thesis: for r being Real st ( for n being Element of NAT holds F . n = A /\ (great_eq_dom f,(R_EAL (r + (1 / (n + 1))))) ) holds
A /\ (great_dom f,(R_EAL r)) = union (rng F)
let r be Real; :: thesis: ( ( for n being Element of NAT holds F . n = A /\ (great_eq_dom f,(R_EAL (r + (1 / (n + 1))))) ) implies A /\ (great_dom f,(R_EAL r)) = union (rng F) )
assume A1: for n being Element of NAT holds F . n = A /\ (great_eq_dom f,(R_EAL (r + (1 / (n + 1))))) ; :: thesis: A /\ (great_dom f,(R_EAL r)) = union (rng F)
A2: for x being set st x in A /\ (great_dom f,(R_EAL r)) holds
x in union (rng F)

proof

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

proof

reconsider x = x as Element of X by A3;
A7: x in dom f by A5, Def14;
A8: R_EAL r < f . x by A5, Def14;
A9: ex m being Element of NAT st R_EAL (r + (1 / (m + 1))) <= f . x

proof

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

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

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

end;

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

A12: not +infty <= f . x by A11, XXREAL_0:4;
reconsider y1 = f . x as Real by A8, A12, XXREAL_0:48;
consider m being Element of NAT such that
A13: 1 / (m + 1) < y1 - r by A8, Th13;
take m ; :: thesis: R_EAL (r + (1 / (m + 1))) <= f . x
thus R_EAL (r + (1 / (m + 1))) <= f . x by A13, XREAL_1:22; :: thesis: verum

end;

end;

end;

consider m being Element of NAT such that
A14: R_EAL (r + (1 / (m + 1))) <= f . x by A9;
A15: x in great_eq_dom f,(R_EAL (r + (1 / (m + 1)))) by A7, A14, Def15;
A16: x in A /\ (great_eq_dom f,(R_EAL (r + (1 / (m + 1))))) by A4, A15, XBOOLE_0:def 4;
A17: m in NAT ;
A18: m in dom F by A17, 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, A16, A18, FUNCT_1:def 5; :: thesis: verum

end;

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

end;

A19: A /\ (great_dom f,(R_EAL r)) c= union (rng F) by A2, TARSKI:def 3;
A20: for x being set st x in union (rng F) holds
x in A /\ (great_dom f,(R_EAL r))

proof

let x be set ; :: thesis: ( x in union (rng F) implies x in A /\ (great_dom f,(R_EAL r)) )
assume A21: x in union (rng F) ; :: thesis: x in A /\ (great_dom f,(R_EAL r))
consider Y being set such that
A22: x in Y and
A23: Y in rng F by A21, TARSKI:def 4;
consider m being Element of NAT such that
m in dom F and
A24: F . m = Y by A23, PARTFUN1:26;
A25: x in A /\ (great_eq_dom f,(R_EAL (r + (1 / (m + 1))))) by A1, A22, A24;
A26: x in A by A25, XBOOLE_0:def 4;
A27: x in great_eq_dom f,(R_EAL (r + (1 / (m + 1)))) by A25, XBOOLE_0:def 4;
A28: x in dom f by A27, Def15;
A29: R_EAL (r + (1 / (m + 1))) <= f . x by A27, Def15;
reconsider x = x as Element of X by A22, A23;
A30: R_EAL r < f . x

proof

A31: now

A33: r < r + (1 / (m + 1)) by XREAL_1:31, XREAL_1:141;
thus R_EAL r < f . x by A29, A33, XXREAL_0:2; :: thesis: verum

end;

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

end;

A34: x in great_dom f,(R_EAL r) by A28, A30, Def14;
thus x in A /\ (great_dom f,(R_EAL r)) by A26, A34, XBOOLE_0:def 4; :: thesis: verum

end;

A35: union (rng F) c= A /\ (great_dom f,(R_EAL r)) by A20, TARSKI:def 3;
thus A /\ (great_dom f,(R_EAL r)) = union (rng F) by A19, A35, XBOOLE_0:def 10; :: thesis: verum