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 /\ (great_dom (f,(R_EAL (- n)))) ) holds
A /\ (great_dom (f,-infty)) = 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 st ( for n being Element of NAT holds F . n = A /\ (great_dom (f,(R_EAL (- n)))) ) holds
A /\ (great_dom (f,-infty)) = union (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 /\ (great_dom (f,(R_EAL (- n)))) ) holds
A /\ (great_dom (f,-infty)) = union (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 /\ (great_dom (f,(R_EAL (- n)))) ) holds
A /\ (great_dom (f,-infty)) = union (rng F)
let A be set ; :: thesis: ( ( for n being Element of NAT holds F . n = A /\ (great_dom (f,(R_EAL (- n)))) ) implies A /\ (great_dom (f,-infty)) = union (rng F) )
assume A1: for n being Element of NAT holds F . n = A /\ (great_dom (f,(R_EAL (- n)))) ; :: thesis: A /\ (great_dom (f,-infty)) = union (rng F)
for x being set st x in A /\ (great_dom (f,-infty)) holds
x in union (rng F)

proof

let x be set ; :: thesis: ( x in A /\ (great_dom (f,-infty)) implies x in union (rng F) )
assume A3: x in A /\ (great_dom (f,-infty)) ; :: thesis: x in union (rng F)
then A4: x in A by XBOOLE_0:def 4;
A5: x in great_dom (f,-infty) by A3, XBOOLE_0:def 4;
then A6: x in dom f by Def14;
A7: -infty < f . x by A5, Def14;
ex n being Element of NAT st R_EAL (- n) < f . x

proof

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

suppose A9: f . x = +infty ; :: thesis: ex n being Element of NAT st R_EAL (- n) < f . x

take 0 ; :: thesis: R_EAL (- 0) < f . x
thus R_EAL (- 0) < f . x by A9; :: thesis: verum

end;

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

then not +infty <= f . x by XXREAL_0:4;
then reconsider y1 = f . x as Real by A7, XXREAL_0:48;
consider n1 being Element of NAT such that
A12: - n1 <= y1 by Th12;
n1 < n1 + 1 by NAT_1:13;
then A14: - (n1 + 1) < - n1 by XREAL_1:26;
reconsider m = n1 + 1 as Element of NAT ;
take m ; :: thesis: R_EAL (- m) < f . x
thus R_EAL (- m) < f . x by A12, A14, XXREAL_0:2; :: thesis: verum

end;

end;

end;

then consider n being Element of NAT such that
A15: R_EAL (- n) < f . x ;
reconsider x = x as Element of X by A3;
x in great_dom (f,(R_EAL (- n))) by A6, A15, Def14;
then x in A /\ (great_dom (f,(R_EAL (- n)))) by A4, XBOOLE_0:def 4;
then A18: x in F . n by A1;
n in NAT ;
then n in dom F by FUNCT_2:def 1;
then F . n in rng F by FUNCT_1:def 5;
hence x in union (rng F) by A18, TARSKI:def 4; :: thesis: verum

end;

then A22: A /\ (great_dom (f,-infty)) c= union (rng F) by TARSKI:def 3;
for x being set st x in union (rng F) holds
x in A /\ (great_dom (f,-infty))

proof

let x be set ; :: thesis: ( x in union (rng F) implies x in A /\ (great_dom (f,-infty)) )
assume x in union (rng F) ; :: thesis: x in A /\ (great_dom (f,-infty))
then consider Y being set such that
A25: x in Y and
A26: Y in rng F by 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 /\ (great_dom (f,(R_EAL (- m)))) by A1, A25, A27;
then A29: x in A by XBOOLE_0:def 4;
A30: x in great_dom (f,(R_EAL (- m))) by A28, XBOOLE_0:def 4;
then A31: x in dom f by Def14;
A32: R_EAL (- m) < f . x by A30, Def14;
reconsider x = x as Element of X by A25, A26;
-infty < f . x by A32, XXREAL_0:2, XXREAL_0:12;
then x in great_dom (f,-infty) by A31, Def14;
hence x in A /\ (great_dom (f,-infty)) by A29, XBOOLE_0:def 4; :: thesis: verum

end;

then union (rng F) c= A /\ (great_dom (f,-infty)) by TARSKI:def 3;
hence A /\ (great_dom (f,-infty)) = union (rng F) by A22, XBOOLE_0:def 10; :: thesis: verum