theorem :: MESFUNC6:10

for X being non empty set
for Y being set
for S being SigmaField of X
for F being sequence of S
for f being PartFunc of X,REAL
for r being Real st ( for n being Nat holds F . n = Y /\ (less_eq_dom (f,(r - (1 / (n + 1))))) ) holds
Y /\ (less_dom (f,r)) = union (rng F)