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