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 st M . E < +infty holds
( chi (E,X) is_integrable_on M & Integral (M,(chi (E,X))) = M . E & Integral (M,((chi (E,X)) | E)) = M . E )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for E being Element of S st M . E < +infty holds
( chi (E,X) is_integrable_on M & Integral (M,(chi (E,X))) = M . E & Integral (M,((chi (E,X)) | E)) = M . E )
let M be sigma_Measure of S; :: thesis: for E being Element of S st M . E < +infty holds
( chi (E,X) is_integrable_on M & Integral (M,(chi (E,X))) = M . E & Integral (M,((chi (E,X)) | E)) = M . E )
let E be Element of S; :: thesis: ( M . E < +infty implies ( chi (E,X) is_integrable_on M & Integral (M,(chi (E,X))) = M . E & Integral (M,((chi (E,X)) | E)) = M . E ) )
reconsider XX = X as Element of S by MEASURE1:21;
set F = XX \ E;

A1: now

let x be Element of X; :: thesis: ( x in dom (max- (chi (E,X))) implies (max- (chi (E,X))) . x = 0 )

A2: now

assume x in E ; :: thesis: max ((- ((chi (E,X)) . x)),0.) = 0.
then (chi (E,X)) . x = 1 by FUNCT_3:def 3;
hence max ((- ((chi (E,X)) . x)),0.) = 0. by XXREAL_0:def 10; :: thesis: verum

end;

A3: now

assume not x in E ; :: thesis: max ((- ((chi (E,X)) . x)),0.) = 0.
then (chi (E,X)) . x = 0. by FUNCT_3:def 3;
then - ((chi (E,X)) . x) = 0 ;
hence max ((- ((chi (E,X)) . x)),0.) = 0. ; :: thesis: verum

end;

assume x in dom (max- (chi (E,X))) ; :: thesis: (max- (chi (E,X))) . x = 0
hence (max- (chi (E,X))) . x = 0 by A2, A3, MESFUNC2:def 3; :: thesis: verum

end;

A4: XX = dom (chi (E,X)) by FUNCT_3:def 3;
then A5: XX = dom (max+ (chi (E,X))) by Th23;
A6: XX /\ (XX \ E) = XX \ E by XBOOLE_1:28;
then A7: dom ((max+ (chi (E,X))) | (XX \ E)) = XX \ E by A5, RELAT_1:90;

A8: now

let x be Element of X; :: thesis: ( x in dom ((max+ (chi (E,X))) | (XX \ E)) implies ((max+ (chi (E,X))) | (XX \ E)) . x = 0 )
assume A9: x in dom ((max+ (chi (E,X))) | (XX \ E)) ; :: thesis: ((max+ (chi (E,X))) | (XX \ E)) . x = 0
then (chi (E,X)) . x = 0 by A7, FUNCT_3:43;
then (max+ (chi (E,X))) . x = 0 by Th23;
hence ((max+ (chi (E,X))) | (XX \ E)) . x = 0 by A9, FUNCT_1:70; :: thesis: verum

end;

A10: chi (E,X) is_measurable_on XX by MESFUNC2:32;
then A11: max+ (chi (E,X)) is_measurable_on XX by Th23;
then max+ (chi (E,X)) is_measurable_on XX \ E by MESFUNC1:34;
then A12: integral+ (M,((max+ (chi (E,X))) | (XX \ E))) = 0 by A5, A6, A7, A8, MESFUNC5:48, MESFUNC5:93;
XX = dom (max- (chi (E,X))) by A4, MESFUNC2:def 3;
then A13: integral+ (M,(max- (chi (E,X)))) = 0 by A4, A10, A1, MESFUNC2:28, MESFUNC5:93;
A14: XX /\ E = E by XBOOLE_1:28;
then A15: dom ((max+ (chi (E,X))) | E) = E by A5, RELAT_1:90;
E \/ (XX \ E) = XX by A14, XBOOLE_1:51;
then A16: (max+ (chi (E,X))) | (E \/ (XX \ E)) = max+ (chi (E,X)) by A5, RELAT_1:98;
A17: for x being set st x in dom (max+ (chi (E,X))) holds
0. <= (max+ (chi (E,X))) . x by MESFUNC2:14;
then A18: max+ (chi (E,X)) is nonnegative by SUPINF_2:71;
then integral+ (M,((max+ (chi (E,X))) | (E \/ (XX \ E)))) = (integral+ (M,((max+ (chi (E,X))) | E))) + (integral+ (M,((max+ (chi (E,X))) | (XX \ E)))) by A5, A11, MESFUNC5:87, XBOOLE_1:79;
then A19: integral+ (M,(max+ (chi (E,X)))) = integral+ (M,((max+ (chi (E,X))) | E)) by A16, A12, XXREAL_3:4;

A20: now

let x be set ; :: thesis: ( x in dom ((max+ (chi (E,X))) | E) implies ((max+ (chi (E,X))) | E) . x = 1 )
assume A21: x in dom ((max+ (chi (E,X))) | E) ; :: thesis: ((max+ (chi (E,X))) | E) . x = 1
then (chi (E,X)) . x = 1 by A15, FUNCT_3:def 3;
then (max+ (chi (E,X))) . x = 1 by Th23;
hence ((max+ (chi (E,X))) | E) . x = 1 by A21, FUNCT_1:70; :: thesis: verum

end;

then (max+ (chi (E,X))) | E is_simple_func_in S by A15, MESFUNC6:2;
then integral+ (M,(max+ (chi (E,X)))) = integral' (M,((max+ (chi (E,X))) | E)) by A18, A19, MESFUNC5:21, MESFUNC5:83;
then A22: integral+ (M,(max+ (chi (E,X)))) = (R_EAL 1) * (M . (dom ((max+ (chi (E,X))) | E))) by A15, A20, MESFUNC5:110;
max+ (chi (E,X)) is_measurable_on E by A11, MESFUNC1:34;
then (max+ (chi (E,X))) | E is_measurable_on E by A5, A14, MESFUNC5:48;
then A23: (chi (E,X)) | E is_measurable_on E by Th23;
(max+ (chi (E,X))) | E is nonnegative by A17, MESFUNC5:21, SUPINF_2:71;
then A24: (chi (E,X)) | E is nonnegative by Th23;
E = dom ((chi (E,X)) | E) by A15, Th23;
then A25: Integral (M,((chi (E,X)) | E)) = integral+ (M,((chi (E,X)) | E)) by A23, A24, MESFUNC5:94;
assume M . E < +infty ; :: thesis: ( chi (E,X) is_integrable_on M & Integral (M,(chi (E,X))) = M . E & Integral (M,((chi (E,X)) | E)) = M . E )
then integral+ (M,(max+ (chi (E,X)))) < +infty by A15, A22, XXREAL_3:92;
hence chi (E,X) is_integrable_on M by A4, A10, A13, MESFUNC5:def 17; :: thesis: ( Integral (M,(chi (E,X))) = M . E & Integral (M,((chi (E,X)) | E)) = M . E )
Integral (M,(chi (E,X))) = (R_EAL 1) * (M . E) by A15, A22, A13, XXREAL_3:15;
hence Integral (M,(chi (E,X))) = M . E by XXREAL_3:92; :: thesis: Integral (M,((chi (E,X)) | E)) = M . E
(chi (E,X)) | E = (max+ (chi (E,X))) | E by Th23;
hence Integral (M,((chi (E,X)) | E)) = M . E by A15, A19, A22, A25, XXREAL_3:92; :: thesis: verum