let X be non empty set ; :: thesis: for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,REAL
for F being SetSequence of S
for r being Real st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),r)) ) holds
union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),r))

let S be SigmaField of X; :: thesis: for f being with_the_same_dom Functional_Sequence of X,REAL
for F being SetSequence of S
for r being Real st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),r)) ) holds
union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),r))

let f be with_the_same_dom Functional_Sequence of X,REAL; :: thesis: for F being SetSequence of S
for r being Real st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),r)) ) holds
union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),r))

let F be SetSequence of S; :: thesis: for r being Real st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),r)) ) holds
union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),r))

let r be Real; :: thesis: ( ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),r)) ) implies union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),r)) )
set E = dom (f . 0);
assume A1: for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),r)) ; :: thesis: union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),r))
now :: thesis: for x being object st x in (dom (f . 0)) /\ (great_dom ((sup f),r)) holds
x in union (rng F)
let x be object ; :: thesis: ( x in (dom (f . 0)) /\ (great_dom ((sup f),r)) implies x in union (rng F) )
assume A2: x in (dom (f . 0)) /\ (great_dom ((sup f),r)) ; :: thesis: x in union (rng F)
then reconsider z = x as Element of X ;
A3: x in dom (f . 0) by ;
x in great_dom ((sup f),r) by ;
then A4: r < (sup f) . z by MESFUNC1:def 13;
ex n being Element of NAT st r < (f # z) . n
proof
assume A5: for n being Element of NAT holds (f # z) . n <= r ; :: thesis: contradiction
for p being ExtReal st p in rng (R_EAL (f # z)) holds
p <= r
proof
let p be ExtReal; :: thesis: ( p in rng (R_EAL (f # z)) implies p <= r )
assume p in rng (R_EAL (f # z)) ; :: thesis: p <= r
then ex n being object st
( n in NAT & (R_EAL (f # z)) . n = p ) by FUNCT_2:11;
hence p <= r by A5; :: thesis: verum
end;
then r is UpperBound of rng (R_EAL (f # z)) by XXREAL_2:def 1;
then A6: sup (rng (R_EAL (f # z))) <= r by XXREAL_2:def 3;
x in dom (sup f) by ;
hence contradiction by A4, A6, Th3; :: thesis: verum
end;
then consider n being Element of NAT such that
A7: r < (f # z) . n ;
A8: x in dom (f . n) by ;
r < (f . n) . z by ;
then A9: x in great_dom ((f . n),r) by ;
A10: F . n in rng F by FUNCT_2:4;
F . n = (dom (f . 0)) /\ (great_dom ((f . n),r)) by A1;
then x in F . n by ;
hence x in union (rng F) by ; :: thesis: verum
end;
then A11: (dom (f . 0)) /\ (great_dom ((sup f),r)) c= union (rng F) ;
now :: thesis: for x being object st x in union (rng F) holds
x in (dom (f . 0)) /\ (great_dom ((sup f),r))
let x be object ; :: thesis: ( x in union (rng F) implies x in (dom (f . 0)) /\ (great_dom ((sup f),r)) )
assume x in union (rng F) ; :: thesis: x in (dom (f . 0)) /\ (great_dom ((sup f),r))
then consider y being set such that
A12: x in y and
A13: y in rng F by TARSKI:def 4;
reconsider z = x as Element of X by ;
consider n being object such that
A14: n in dom F and
A15: y = F . n by ;
reconsider n = n as Element of NAT by A14;
A16: F . n = (dom (f . 0)) /\ (great_dom ((f . n),r)) by A1;
then x in great_dom ((f . n),r) by ;
then A17: r < (f . n) . z by MESFUNC1:def 13;
f # z = () # z by Th1;
then (f . n) . z = (() # z) . n by SEQFUNC:def 10;
then A18: (f . n) . z <= sup (rng (() # z)) by ;
A19: x in dom (f . 0) by ;
then A20: x in dom (sup f) by MESFUNC8:def 4;
then (sup f) . z = sup (() # z) by MESFUNC8:def 4;
then r < (sup f) . z by ;
then x in great_dom ((sup f),r) by ;
hence x in (dom (f . 0)) /\ (great_dom ((sup f),r)) by ; :: thesis: verum
end;
then union (rng F) c= (dom (f . 0)) /\ (great_dom ((sup f),r)) ;
hence union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),r)) by A11; :: thesis: verum