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_{3} -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_{2} -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_{1} -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;

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

for M being sigma_Measure of S

for E being Element of S

for f being b

( 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

( 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

( 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 A6:
M . ((eq_dom (f,+infty)) \/ (eq_dom (f,-infty))) = 0
; :: thesis: f is_a.e.finite Massume
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 ) ;

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;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 )

then
E01 \/ E02 c= A
;( 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;( 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

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

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

y in REAL

then
rng (f | ((E01 \/ E02) `)) c= REAL
;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;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

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