let X be 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
let S be 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
let E be 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
let F, G be 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
let n be Nat; ( 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 ) ) implies G . n is E -measurable )
assume that
A1:
F is with_the_same_dom
and
A2:
E c= dom (F . 0)
and
A3:
for m being Nat holds
( F . m is E -measurable & G . m = (F . m) | E )
; G . n is E -measurable
dom (F . n) = dom (F . 0)
by A1;
then
(dom (F . n)) /\ E = E
by A2, XBOOLE_1:28;
then
(F . n) | E is E -measurable
by A3, MESFUNC5:42;
hence
G . n is E -measurable
by A3; verum