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

let x be set ; :: thesis:
assume A2: x in (dom (f . 0 )) /\ (great_dom (sup f),r) ; :: thesis:
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 by A2, XBOOLE_0:def 4;
then A4: r < (sup f) . z by MESFUNC1:def 14;
ex n being Element of NAT st r < (f # z) . n

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

let p be ext-real number ; :: thesis:
assume p in rng (R_EAL (f # z)) ; :: thesis:
then ex n being set st
( n in NAT & (R_EAL (f # z)) . n = p ) by FUNCT_2:17;
hence p <= r by A5; :: thesis:

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 A3, MESFUNC8:def 4;
hence contradiction by A4, A6, Th3; :: thesis:

end;

then consider n being Element of NAT such that
A7: r < (f # z) . n ;
A8: x in dom (f . n) by A3, MESFUNC8:def 2;
r < (f . n) . z by A7, SEQFUNC:def 11;
then A9: x in great_dom (f . n),r by A8, MESFUNC1:def 14;
A10: F . n in rng F by FUNCT_2:6;
F . n = (dom (f . 0 )) /\ (great_dom (f . n),r) by A1;
then x in F . n by A3, A9, XBOOLE_0:def 4;
hence x in union (rng F) by A10, TARSKI:def 4; :: thesis:

end;

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

let x be set ; :: thesis:
assume x in union (rng F) ; :: thesis:
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 A12, A13;
consider n being set such that
A14: n in dom F and
A15: y = F . n by A13, FUNCT_1:def 5;
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 A12, A15, XBOOLE_0:def 4;
then A17: r < (f . n) . z by MESFUNC1:def 14;
f # z = (R_EAL f) # z by Th1;
then (f . n) . z = ((R_EAL f) # z) . n by SEQFUNC:def 11;
then A18: (f . n) . z <= sup (rng ((R_EAL f) # z)) by FUNCT_2:6, XXREAL_2:4;
A19: x in dom (f . 0 ) by A12, A15, A16, XBOOLE_0:def 4;
then A20: x in dom (sup f) by MESFUNC8:def 4;
then (sup f) . z = sup ((R_EAL f) # z) by MESFUNC8:def 4;
then r < (sup f) . z by A17, A18, XXREAL_0:2;
then x in great_dom (sup f),r by A20, MESFUNC1:def 14;
hence x in (dom (f . 0 )) /\ (great_dom (sup f),r) by A19, XBOOLE_0:def 4; :: thesis:

end;

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