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

proof

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

proof

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

suppose A7: f . x = -infty ; :: thesis: ex n being Element of NAT st f . x < R_EAL n

take 0 ; :: thesis: f . x < R_EAL 0
thus f . x < R_EAL 0 by A7; :: thesis: verum

end;

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

then not f . x <= -infty by XXREAL_0:6;
then reconsider y1 = f . x as Real by A6, XXREAL_0:48;
consider n1 being Element of NAT such that
A8: y1 <= n1 by Th11;
A9: n1 < n1 + 1 by NAT_1:13;
reconsider m = n1 + 1 as Element of NAT ;
take m ; :: thesis: f . x < R_EAL m
thus f . x < R_EAL m by A8, A9, XXREAL_0:2; :: thesis: verum

end;

end;

end;

then consider n being Element of NAT such that
A10: f . x < R_EAL n ;
reconsider x = x as Element of X by A2;
x in less_dom (f,(R_EAL n)) by A5, A10, Def12;
then x in A /\ (less_dom (f,(R_EAL n))) by A3, XBOOLE_0:def 4;
then A11: 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 3;
hence x in union (rng F) by A11, TARSKI:def 4; :: thesis: verum

end;

then A12: A /\ (less_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 /\ (less_dom (f,+infty))

proof

let x be set ; :: thesis: ( x in union (rng F) implies x in A /\ (less_dom (f,+infty)) )
assume x in union (rng F) ; :: thesis: x in A /\ (less_dom (f,+infty))
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_dom (f,(R_EAL m))) by A1, A13, A15;
then A17: x in A by XBOOLE_0:def 4;
A18: x in less_dom (f,(R_EAL m)) by A16, XBOOLE_0:def 4;
then A19: x in dom f by Def12;
A20: f . x < R_EAL m by A18, Def12;
reconsider x = x as Element of X by A13, A14;
f . x < +infty by A20, XXREAL_0:2, XXREAL_0:9;
then x in less_dom (f,+infty) by A19, Def12;
hence x in A /\ (less_dom (f,+infty)) by A17, XBOOLE_0:def 4; :: thesis: verum

end;

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