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)
A2: 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 A3: x in A /\ (less_dom f,+infty ) ; :: thesis: x in union (rng F)
A4: x in A by A3, XBOOLE_0:def 4;
A5: x in less_dom f,+infty by A3, XBOOLE_0:def 4;
A6: x in dom f by A5, Def12;
A7: f . x < +infty by A5, Def12;
A8: ex n being Element of NAT st f . x < R_EAL n

proof

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

suppose A9: 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 A9; :: thesis: verum

end;

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

A11: not f . x <= -infty by A10, XXREAL_0:6;
reconsider y1 = f . x as Real by A7, A11, XXREAL_0:48;
consider n1 being Element of NAT such that
A12: y1 <= n1 by Th11;
A13: 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 A12, A13, XXREAL_0:2; :: thesis: verum

end;

end;

end;

consider n being Element of NAT such that
A14: f . x < R_EAL n by A8;
reconsider x = x as Element of X by A3;
A15: x in less_dom f,(R_EAL n) by A6, A14, Def12;
A16: x in A /\ (less_dom f,(R_EAL n)) by A4, A15, XBOOLE_0:def 4;
A17: x in F . n by A1, A16;
A18: n in NAT ;
A19: n in dom F by A18, FUNCT_2:def 1;
A20: F . n in rng F by A19, FUNCT_1:def 5;
thus x in union (rng F) by A17, A20, TARSKI:def 4; :: thesis: verum

end;

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

end;

A34: union (rng F) c= A /\ (less_dom f,+infty ) by A22, TARSKI:def 3;
thus A /\ (less_dom f,+infty ) = union (rng F) by A21, A34, XBOOLE_0:def 10; :: thesis: verum