theorem :: MESFUNC6:11

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 /\ (great_eq_dom (f,(r + (1 / (n + 1))))) ) holds
Y /\ (great_dom (f,r)) = union (rng F)