theorem Th26: :: MESFUNC1:26

for X being set
for S being SigmaField of X
for F being sequence of S
for f being PartFunc of X,ExtREAL
for A being set st ( for n being Element of NAT holds F . n = A /\ (great_dom (f,(- n))) ) holds
A /\ (great_dom (f,-infty)) = union (rng F)