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))

hence union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),r)) by A11; :: thesis: verum

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)

then A11:
(dom (f . 0)) /\ (great_dom ((sup f),r)) c= union (rng F)
;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 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 13;

ex n being Element of NAT st r < (f # z) . n

A7: r < (f # z) . n ;

A8: x in dom (f . n) by A3, MESFUNC8:def 2;

r < (f . n) . z by A7, SEQFUNC:def 10;

then A9: x in great_dom ((f . n),r) by A8, MESFUNC1:def 13;

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 A3, A9, XBOOLE_0:def 4;

hence x in union (rng F) by A10, TARSKI:def 4; :: thesis: verum

end;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 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 13;

ex n being Element of NAT st r < (f # z) . n

proof

then consider n being Element of NAT such that
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

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: verum

end;for p being ExtReal st p in rng (R_EAL (f # z)) holds

p <= r

proof

then
r is UpperBound of rng (R_EAL (f # z))
by XXREAL_2:def 1;
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;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

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: verum

A7: r < (f # z) . n ;

A8: x in dom (f . n) by A3, MESFUNC8:def 2;

r < (f . n) . z by A7, SEQFUNC:def 10;

then A9: x in great_dom ((f . n),r) by A8, MESFUNC1:def 13;

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 A3, A9, XBOOLE_0:def 4;

hence x in union (rng F) by A10, TARSKI:def 4; :: thesis: verum

now :: thesis: for x being object st x in union (rng F) holds

x in (dom (f . 0)) /\ (great_dom ((sup f),r))

then
union (rng F) c= (dom (f . 0)) /\ (great_dom ((sup f),r))
;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 A12, A13;

consider n being object such that

A14: n in dom F and

A15: y = F . n by A13, FUNCT_1:def 3;

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 13;

f # z = (R_EAL f) # z by Th1;

then (f . n) . z = ((R_EAL f) # z) . n by SEQFUNC:def 10;

then A18: (f . n) . z <= sup (rng ((R_EAL f) # z)) by FUNCT_2:4, 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 13;

hence x in (dom (f . 0)) /\ (great_dom ((sup f),r)) by A19, XBOOLE_0:def 4; :: thesis: verum

end;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 A12, A13;

consider n being object such that

A14: n in dom F and

A15: y = F . n by A13, FUNCT_1:def 3;

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 13;

f # z = (R_EAL f) # z by Th1;

then (f . n) . z = ((R_EAL f) # z) . n by SEQFUNC:def 10;

then A18: (f . n) . z <= sup (rng ((R_EAL f) # z)) by FUNCT_2:4, 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 13;

hence x in (dom (f . 0)) /\ (great_dom ((sup f),r)) by A19, XBOOLE_0:def 4; :: thesis: verum

hence union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),r)) by A11; :: thesis: verum