let X be non empty set ; 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 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; for f being with_the_same_dom Functional_Sequence of X,ExtREAL
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,ExtREAL; 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; 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; ( ( 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))
; union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),r))
now 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 ;
( 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))
;
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 . n) . z
then consider n being
Element of
NAT such that A9:
r < (f . n) . z
;
x in dom (f . n)
by A3, Def2;
then A10:
x in great_dom (
(f . n),
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))
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;
verum end;
then A13:
(dom (f . 0)) /\ (great_dom ((sup f),r)) c= union (rng F)
;
now 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 ;
( x in union (rng F) implies x in (dom (f . 0)) /\ (great_dom ((sup f),r)) )assume
x in union (rng F)
;
x in (dom (f . 0)) /\ (great_dom ((sup f),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
object 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))
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 < (sup f) . z
by A19, XXREAL_0:2;
then
x in great_dom (
(sup f),
r)
by A22, MESFUNC1:def 13;
hence
x in (dom (f . 0)) /\ (great_dom ((sup f),r))
by A21, XBOOLE_0:def 4;
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 A13, XBOOLE_0:def 10; verum