theorem Th20: :: MESFUNC9:20

for X being non empty set
for S being SigmaField of X
for E being Element of S
for F, G being Functional_Sequence of X,ExtREAL
for n being Nat st F is with_the_same_dom & E c= dom (F . 0) & ( for m being Nat holds
( F . m is E -measurable & G . m = (F . m) | E ) ) holds
G . n is E -measurable