theorem Th19: :: MESFUNC8:19

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 E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is E -measurable ) holds
for n being Nat holds (superior_realsequence f) . n is E -measurable