let X be non empty set ; :: thesis: for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for F being SetSequence of S
for r being real number st ( for n being natural number holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),(R_EAL r))) ) holds
union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),(R_EAL r)))
let S be SigmaField of X; :: thesis: for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for F being SetSequence of S
for r being real number st ( for n being natural number holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),(R_EAL r))) ) holds
union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),(R_EAL r)))
let f be with_the_same_dom Functional_Sequence of X,ExtREAL; :: thesis: for F being SetSequence of S
for r being real number st ( for n being natural number holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),(R_EAL r))) ) holds
union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),(R_EAL r)))
let F be SetSequence of S; :: thesis: for r being real number st ( for n being natural number holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),(R_EAL r))) ) holds
union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),(R_EAL r)))
let r be real number ; :: thesis: ( ( for n being natural number holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),(R_EAL r))) ) implies union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),(R_EAL r))) )
set E = dom (f . 0);
assume A1: for n being natural number holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),(R_EAL r))) ; :: thesis: union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),(R_EAL r)))

now

let x be set ; :: thesis: ( x in (dom (f . 0)) /\ (great_dom ((sup f),(R_EAL r))) implies x in union (rng F) )
assume A2: x in (dom (f . 0)) /\ (great_dom ((sup f),(R_EAL r))) ; :: thesis: x in union (rng F)
then reconsider z = x as Element of X ;
A3: x in dom (f . 0) by A2, XBOOLE_0:def 4;
x in great_dom ((sup f),(R_EAL r)) by A2, XBOOLE_0:def 4;
then A4: R_EAL r < (sup f) . z by MESFUNC1:def 13;
ex n being Element of NAT st R_EAL r < (f . n) . z

proof

assume A5: for n being Element of NAT holds (f . n) . z <= R_EAL r ; :: thesis: contradiction
for x being ext-real number st x in rng (f # z) holds
x <= R_EAL r

proof

let x be ext-real number ; :: thesis: ( x in rng (f # z) implies x <= R_EAL r )
assume x in rng (f # z) ; :: thesis: x <= R_EAL r
then consider m being set such that
A6: m in NAT and
A7: x = (f # z) . m by FUNCT_2:11;
reconsider m = m as Element of NAT by A6;
x = (f . m) . z by A7, MESFUNC5:def 13;
hence x <= R_EAL r by A5; :: thesis: verum

end;

then R_EAL r is UpperBound of rng (f # z) by XXREAL_2:def 1;
then A8: sup (f # z) <= R_EAL r by XXREAL_2:def 3;
x in dom (sup f) by A3, Def4;
hence contradiction by A4, A8, Def4; :: thesis: verum

end;

then consider n being Element of NAT such that
A9: R_EAL r < (f . n) . z ;
x in dom (f . n) by A3, Def2;
then A10: x in great_dom ((f . n),(R_EAL r)) by A9, MESFUNC1:def 13;
A11: F . n in rng F by FUNCT_2:4;
A12: F . n = (dom (f . 0)) /\ (great_dom ((f . n),(R_EAL r))) by A1;
x in dom (f . 0) by A2, XBOOLE_0:def 4;
then x in F . n by A10, A12, XBOOLE_0:def 4;
hence x in union (rng F) by A11, TARSKI:def 4; :: thesis: verum

end;

then A13: (dom (f . 0)) /\ (great_dom ((sup f),(R_EAL r))) c= union (rng F) by TARSKI:def 3;

now

let x be set ; :: thesis: ( x in union (rng F) implies x in (dom (f . 0)) /\ (great_dom ((sup f),(R_EAL r))) )
assume x in union (rng F) ; :: thesis: x in (dom (f . 0)) /\ (great_dom ((sup f),(R_EAL r)))
then consider y being set such that
A14: x in y and
A15: y in rng F by TARSKI:def 4;
reconsider z = x as Element of X by A14, A15;
consider n being set such that
A16: n in dom F and
A17: y = F . n by A15, FUNCT_1:def 3;
reconsider n = n as Element of NAT by A16;
A18: F . n = (dom (f . 0)) /\ (great_dom ((f . n),(R_EAL r))) by A1;
then x in great_dom ((f . n),r) by A14, A17, XBOOLE_0:def 4;
then A19: r < (f . n) . z by MESFUNC1:def 13;
A20: (f . n) . z = (f # z) . n by MESFUNC5:def 13;
A21: x in dom (f . 0) by A14, A17, A18, XBOOLE_0:def 4;
then A22: x in dom (sup f) by Def4;
then (sup f) . z = sup (f # z) by Def4;
then (f . n) . z <= (sup f) . z by A20, RINFSUP2:23;
then R_EAL r < (sup f) . z by A19, XXREAL_0:2;
then x in great_dom ((sup f),(R_EAL r)) by A22, MESFUNC1:def 13;
hence x in (dom (f . 0)) /\ (great_dom ((sup f),(R_EAL r))) by A21, XBOOLE_0:def 4; :: thesis: verum

end;

then union (rng F) c= (dom (f . 0)) /\ (great_dom ((sup f),(R_EAL r))) by TARSKI:def 3;
hence union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),(R_EAL r))) by A13, XBOOLE_0:def 10; :: thesis: verum