theorem Th24: :: MESFUNC1:24

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 /\ (less_dom (f,n)) ) holds
A /\ (less_dom (f,+infty)) = union (rng F)