let X be non empty set ; :: thesis: for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,REAL
for E being Element of S st dom (f . 0 ) = E & ( for n being natural number holds f . n is_measurable_on E ) holds
lim_sup f is_measurable_on E
let S be SigmaField of X; :: thesis: for f being with_the_same_dom Functional_Sequence of X,REAL
for E being Element of S st dom (f . 0 ) = E & ( for n being natural number holds f . n is_measurable_on E ) holds
lim_sup f is_measurable_on E
let f be with_the_same_dom Functional_Sequence of X,REAL ; :: thesis: for E being Element of S st dom (f . 0 ) = E & ( for n being natural number holds f . n is_measurable_on E ) holds
lim_sup f is_measurable_on E
let E be Element of S; :: thesis: ( dom (f . 0 ) = E & ( for n being natural number holds f . n is_measurable_on E ) implies lim_sup f is_measurable_on E )
assume A1: ( dom (f . 0 ) = E & ( for n being natural number holds f . n is_measurable_on E ) ) ; :: thesis: lim_sup f is_measurable_on E
for n being natural number holds (R_EAL f) . n is_measurable_on E by A1, LEM4;
hence lim_sup f is_measurable_on E by A1, MESFUNC8:23; :: thesis: verum