let X be non empty set ; for S being SigmaField of X
for E being Element of S
for f being b2 -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; for E being Element of S
for f being b1 -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; 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; ( dom f = E implies ( eq_dom (f,+infty) in S & eq_dom (f,-infty) in S ) )
assume A1:
dom f = E
; ( 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; verum