let X be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: 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; :: thesis: verum