let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for f being b₃ -measurable PartFunc of X,ExtREAL st dom f = E holds
( f is_a.e.finite M iff M . ((eq_dom (f,+infty)) \/ (eq_dom (f,-infty))) = 0 )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for E being Element of S
for f being b₂ -measurable PartFunc of X,ExtREAL st dom f = E holds
( f is_a.e.finite M iff M . ((eq_dom (f,+infty)) \/ (eq_dom (f,-infty))) = 0 )
let M be sigma_Measure of S; :: thesis: for E being Element of S
for f being b₁ -measurable PartFunc of X,ExtREAL st dom f = E holds
( f is_a.e.finite M iff M . ((eq_dom (f,+infty)) \/ (eq_dom (f,-infty))) = 0 )
let E be Element of S; :: thesis: for f being E -measurable PartFunc of X,ExtREAL st dom f = E holds
( f is_a.e.finite M iff M . ((eq_dom (f,+infty)) \/ (eq_dom (f,-infty))) = 0 )
let f be E -measurable PartFunc of X,ExtREAL; :: thesis: ( dom f = E implies ( f is_a.e.finite M iff M . ((eq_dom (f,+infty)) \/ (eq_dom (f,-infty))) = 0 ) )
assume dom f = E ; :: thesis: ( f is_a.e.finite M iff M . ((eq_dom (f,+infty)) \/ (eq_dom (f,-infty))) = 0 )
then reconsider E01 = eq_dom (f,+infty), E02 = eq_dom (f,-infty) as Element of S by Th9;
A1: ( E01 c= dom f & E02 c= dom f ) by MESFUNC1:def 15;

hereby :: thesis: ( M . ((eq_dom (f,+infty)) \/ (eq_dom (f,-infty))) = 0 implies f is_a.e.finite M )

assume f is_a.e.finite M ; :: thesis: M . ((eq_dom (f,+infty)) \/ (eq_dom (f,-infty))) = 0
then consider A being Element of S such that
A2: ( M . A = 0 & A c= dom f & f | (A `) is PartFunc of X,REAL ) ;

now :: thesis: for x being object holds
( not x in E01 \/ E02 or x in A )

assume ex x being object st
( x in E01 \/ E02 & not x in A ) ; :: thesis: contradiction
then consider x being object such that
A3: ( x in E01 \/ E02 & not x in A ) ;
( x in E01 or x in E02 ) by A3, XBOOLE_0:def 3;
then A4: ( x in dom f & ( f . x = +infty or f . x = -infty ) ) by MESFUNC1:def 15;
x in X \ A by A3, XBOOLE_0:def 5;
then A5: x in A ` by SUBSET_1:def 4;
then x in dom (f | (A `)) by A4, RELAT_1:57;
then (f | (A `)) . x in REAL by A2, PARTFUN1:4;
hence contradiction by A4, A5, FUNCT_1:49; :: thesis: verum

end;

then E01 \/ E02 c= A ;
then M . (E01 \/ E02) <= 0 by A2, MEASURE1:8;
hence M . ((eq_dom (f,+infty)) \/ (eq_dom (f,-infty))) = 0 by MEASURE1:def 2; :: thesis: verum

end;

assume A6: M . ((eq_dom (f,+infty)) \/ (eq_dom (f,-infty))) = 0 ; :: thesis: f is_a.e.finite M

now :: thesis: for y being object st y in rng (f | ((E01 \/ E02) `)) holds
y in REAL

let y be object ; :: thesis: ( y in rng (f | ((E01 \/ E02) `)) implies y in REAL )
assume y in rng (f | ((E01 \/ E02) `)) ; :: thesis: y in REAL
then consider x being object such that
A7: ( x in dom (f | ((E01 \/ E02) `)) & (f | ((E01 \/ E02) `)) . x = y ) by FUNCT_1:def 3;
dom (f | ((E01 \/ E02) `)) c= (E01 \/ E02) ` by RELAT_1:58;
then x in (E01 \/ E02) ` by A7;
then x in X \ (E01 \/ E02) by SUBSET_1:def 4;
then not x in E01 \/ E02 by XBOOLE_0:def 5;
then A8: ( not x in E01 & not x in E02 ) by XBOOLE_0:def 3;
dom (f | ((E01 \/ E02) `)) c= dom f by RELAT_1:60;
then ( f . x <> +infty & f . x <> -infty ) by A7, A8, MESFUNC1:def 15;
then f . x in REAL by XXREAL_0:14;
hence y in REAL by A7, FUNCT_1:47; :: thesis: verum

end;

then rng (f | ((E01 \/ E02) `)) c= REAL ;
then f | ((E01 \/ E02) `) is PartFunc of X,REAL by RELSET_1:6;
hence f is_a.e.finite M by A1, A6, XBOOLE_1:8; :: thesis: verum