theorem Th4: :: MESFUN9C:4

for X being non empty set
for S being SigmaField of X
for E being Element of S
for F being Functional_Sequence of X,REAL
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 ) holds
(F || E) . n is E -measurable