theorem Th18: :: MESFUNC8:18

for X being 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_eq_dom ((f . n),r)) ) holds
for n being Nat holds (inferior_setsequence F) . n = (dom (f . 0)) /\ (great_eq_dom (((inferior_realsequence f) . n),r))