let X be non empty set ; :: thesis: for S being SigmaField of X
for E being Element of S
for f being b₂ -measurable PartFunc of X,ExtREAL st dom f = E holds
( eq_dom (f,+infty) in S & eq_dom (f,-infty) in S )
let S be SigmaField of X; :: thesis: for E being Element of S
for f being b₁ -measurable PartFunc of X,ExtREAL st dom f = E holds
( eq_dom (f,+infty) in S & eq_dom (f,-infty) in S )
let E be Element of S; :: thesis: for f being E -measurable PartFunc of X,ExtREAL st dom f = E holds
( eq_dom (f,+infty) in S & eq_dom (f,-infty) in S )
let f be E -measurable PartFunc of X,ExtREAL; :: thesis: ( dom f = E implies ( eq_dom (f,+infty) in S & eq_dom (f,-infty) in S ) )
assume A1: dom f = E ; :: thesis: ( eq_dom (f,+infty) in S & eq_dom (f,-infty) in S )
then A2: ( eq_dom (f,+infty) c= E & eq_dom (f,-infty) c= E ) by MESFUNC1:def 15;
( E /\ (eq_dom (f,+infty)) in S & E /\ (eq_dom (f,-infty)) in S ) by A1, MESFUNC1:33, MESFUNC1:34;
hence ( eq_dom (f,+infty) in S & eq_dom (f,-infty) in S ) by A2, XBOOLE_1:28; :: thesis: verum