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
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
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
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 ; :: 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 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
A2: ( x in y & y in rng F ) by TARSKI:def 4;
consider n being set such that
A3: ( n in dom F & y = F . n ) by A2, FUNCT_1:def 5;
reconsider z = x as Element of X by A2;
reconsider n = n as Element of NAT by A3;
F . n = (dom (f . 0 )) /\ (great_dom (f . n),(R_EAL r)) by A1;
then A4: ( x in dom (f . 0 ) & x in great_dom (f . n),r ) by A2, A3, XBOOLE_0:def 4;
then A5: r < (f . n) . z by MESFUNC1:def 14;
A6: x in dom (sup f) by A4, Def4;
then A7: (sup f) . z = sup (f # z) by Def4;
(f . n) . z = (f # z) . n by MESFUNC5:def 13;
then (f . n) . z <= (sup f) . z by A7, RINFSUP2:23;
then R_EAL r < (sup f) . z by A5, XXREAL_0:2;
then x in great_dom (sup f),(R_EAL r) by A6, MESFUNC1:def 14;
hence x in (dom (f . 0 )) /\ (great_dom (sup f),(R_EAL r)) by A4, XBOOLE_0:def 4; :: thesis: verum

end;

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

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 A9: 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 ;
A10: ( x in dom (f . 0 ) & x in great_dom (sup f),(R_EAL r) ) by A9, XBOOLE_0:def 4;
then A11: R_EAL r < (sup f) . z by MESFUNC1:def 14;
ex n being Element of NAT st R_EAL r < (f . n) . z

proof

assume A12: 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
A13: ( m in NAT & x = (f # z) . m ) by FUNCT_2:17;
reconsider m = m as Element of NAT by A13;
x = (f . m) . z by A13, MESFUNC5:def 13;
hence x <= R_EAL r by A12; :: thesis: verum

end;

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

end;

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

end;

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