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_measurable_on E & G . m = (F . m) | E ) ) holds
G . n is_measurable_on E
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_measurable_on E & G . m = (F . m) | E ) ) holds
G . n is_measurable_on E
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_measurable_on E & G . m = (F . m) | E ) ) holds
G . n is_measurable_on E
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_measurable_on E & G . m = (F . m) | E ) ) holds
G . n is_measurable_on E
let n be Nat; :: thesis: ( F is with_the_same_dom & E c= dom (F . 0) & ( for m being Nat holds
( F . m is_measurable_on E & G . m = (F . m) | E ) ) implies G . n is_measurable_on E )
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_measurable_on E & G . m = (F . m) | E ) ; :: thesis: G . n is_measurable_on E
dom (F . n) = dom (F . 0) by A1, MESFUNC8:def 2;
then (dom (F . n)) /\ E = E by A2, XBOOLE_1:28;
then (F . n) | E is_measurable_on E by A3, MESFUNC5:42;
hence G . n is_measurable_on E by A3; :: thesis: verum