let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for A being Element of S holds
( ( M . A <> 0 implies Integral (M,(Xchi (A,X))) = +infty ) & ( M . A = 0 implies Integral (M,(Xchi (A,X))) = 0 ) )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for A being Element of S holds
( ( M . A <> 0 implies Integral (M,(Xchi (A,X))) = +infty ) & ( M . A = 0 implies Integral (M,(Xchi (A,X))) = 0 ) )
let M be sigma_Measure of S; :: thesis: for A being Element of S holds
( ( M . A <> 0 implies Integral (M,(Xchi (A,X))) = +infty ) & ( M . A = 0 implies Integral (M,(Xchi (A,X))) = 0 ) )
let A be Element of S; :: thesis: ( ( M . A <> 0 implies Integral (M,(Xchi (A,X))) = +infty ) & ( M . A = 0 implies Integral (M,(Xchi (A,X))) = 0 ) )
reconsider XX = X as Element of S by MEASURE1:7;
N6: XX = dom (Xchi (A,X)) by FUNCT_2:def 1;

hereby :: thesis: ( M . A = 0 implies Integral (M,(Xchi (A,X))) = 0 )

assume Q1: M . A <> 0 ; :: thesis: Integral (M,(Xchi (A,X))) = +infty

now :: thesis: for x being object st x in eq_dom ((Xchi (A,X)),+infty) holds
x in A

let x be object ; :: thesis: ( x in eq_dom ((Xchi (A,X)),+infty) implies x in A )
assume x in eq_dom ((Xchi (A,X)),+infty) ; :: thesis: x in A
then ( x in dom (Xchi (A,X)) & (Xchi (A,X)) . x = +infty ) by MESFUNC1:def 15;
hence x in A by DefXchi; :: thesis: verum

end;

then Q3: eq_dom ((Xchi (A,X)),+infty) c= A ;

now :: thesis: for x being object st x in A holds
x in eq_dom ((Xchi (A,X)),+infty)

let x be object ; :: thesis: ( x in A implies x in eq_dom ((Xchi (A,X)),+infty) )
assume Q4: x in A ; :: thesis: x in eq_dom ((Xchi (A,X)),+infty)
then x in X ;
then Q6: x in dom (Xchi (A,X)) by FUNCT_2:def 1;
(Xchi (A,X)) . x = +infty by Q4, DefXchi;
hence x in eq_dom ((Xchi (A,X)),+infty) by Q6, MESFUNC1:def 15; :: thesis: verum

end;

then A c= eq_dom ((Xchi (A,X)),+infty) ;
then WW: XX /\ (eq_dom ((Xchi (A,X)),+infty)) = A by Q3, XBOOLE_1:28;
Xchi (A,X) is XX -measurable by Th32;
hence Integral (M,(Xchi (A,X))) = +infty by Q1, N6, MESFUNC9:13, WW; :: thesis: verum

end;

assume M5: M . A = 0 ; :: thesis: Integral (M,(Xchi (A,X))) = 0
reconsider XDn = XX \ A as Element of S ;
reconsider F = (Xchi (A,X)) | A as PartFunc of X,ExtREAL by PARTFUN1:11;
reconsider F1 = (Xchi (A,X)) | XDn as PartFunc of X,ExtREAL by PARTFUN1:11;
reconsider F2 = (Xchi (A,X)) | (XDn \/ A) as PartFunc of X,ExtREAL by PARTFUN1:11;
ZZ: ex E being Element of S st
( E = dom (Xchi (A,X)) & Xchi (A,X) is E -measurable )

proof

take XX ; :: thesis: ( XX = dom (Xchi (A,X)) & Xchi (A,X) is XX -measurable )
thus ( XX = dom (Xchi (A,X)) & Xchi (A,X) is XX -measurable ) by N6, Th32; :: thesis: verum

end;

then M4: Integral (M,F) = 0 by M5, MESFUNC5:94;
N1: XDn = dom ((Xchi (A,X)) | XDn) by FUNCT_2:def 1;
MM: XDn = (dom (Xchi (A,X))) /\ XDn by N6, XBOOLE_1:28;
Xchi (A,X) is XDn -measurable by Th32;
then N2: F1 is XDn -measurable by MM, MESFUNC5:42;
for x being Element of X st x in dom ((Xchi (A,X)) | XDn) holds
((Xchi (A,X)) | XDn) . x = 0

proof

let x be Element of X; :: thesis: ( x in dom ((Xchi (A,X)) | XDn) implies ((Xchi (A,X)) | XDn) . x = 0 )
assume N31: x in dom ((Xchi (A,X)) | XDn) ; :: thesis: ((Xchi (A,X)) | XDn) . x = 0
then not x in A by XBOOLE_0:def 5;
then (Xchi (A,X)) . x = 0 by DefXchi;
hence ((Xchi (A,X)) | XDn) . x = 0 by N31, FUNCT_1:47; :: thesis: verum

end;

then N4: integral+ (M,F1) = 0 by N1, N2, MESFUNC5:87;
N5: Integral (M,F1) = 0 by N1, N2, N4, MESFUNC5:15, MESFUNC5:88;
XDn \/ A = XX \/ A by XBOOLE_1:39;
then N10: XDn \/ A = XX by XBOOLE_1:12;
XDn misses A by XBOOLE_1:79;
then Integral (M,F2) = (Integral (M,F1)) + (Integral (M,F)) by ZZ, MESFUNC5:91;
then Integral (M,F2) = (Integral (M,F1)) + 0 by M4;
hence Integral (M,(Xchi (A,X))) = 0 by N5, N10; :: thesis: verum