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 holds
( 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 holds
( 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 holds
( Integral (M,(chi (E,X))) = M . E & Integral (M,((chi (E,X)) | E)) = M . E )
let E be Element of S; :: thesis: ( Integral (M,(chi (E,X))) = M . E & Integral (M,((chi (E,X)) | E)) = M . E )
reconsider XX = X as Element of S by MEASURE1:7;
set F = XX \ E;

A1: now :: thesis: for x being Element of X st x in dom (max- (chi (E,X))) holds
(max- (chi (E,X))) . x = 0

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

per cases ( x in E or not x in E ) ;

suppose x in E ; :: thesis: (max- (chi (E,X))) . b₁ = 0

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

end;

suppose not x in E ; :: thesis: (max- (chi (E,X))) . b₁ = 0

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

end;

end;

end;

A3: XX = dom (chi (E,X)) by FUNCT_3:def 3;
then A4: XX = dom (max+ (chi (E,X))) by MESFUNC7:23;
A5: XX /\ (XX \ E) = XX \ E by XBOOLE_1:28;
then A6: dom ((max+ (chi (E,X))) | (XX \ E)) = XX \ E by A4, RELAT_1:61;

A7: now :: thesis: for x being Element of X st x in dom ((max+ (chi (E,X))) | (XX \ E)) holds
((max+ (chi (E,X))) | (XX \ E)) . x = 0

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 A8: 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 A6, FUNCT_3:37;
then (max+ (chi (E,X))) . x = 0 by MESFUNC7:23;
hence ((max+ (chi (E,X))) | (XX \ E)) . x = 0 by A8, FUNCT_1:47; :: thesis: verum

end;

A9: chi (E,X) is XX -measurable by MESFUNC2:29;
then A10: max+ (chi (E,X)) is XX -measurable by MESFUNC7:23;
then max+ (chi (E,X)) is XX \ E -measurable by MESFUNC1:30;
then A11: integral+ (M,((max+ (chi (E,X))) | (XX \ E))) = 0 by A4, A5, A6, A7, MESFUNC5:42, MESFUNC5:87;
A12: XX /\ E = E by XBOOLE_1:28;
then A13: dom ((max+ (chi (E,X))) | E) = E by A4, RELAT_1:61;
E \/ (XX \ E) = XX by A12, XBOOLE_1:51;
then A14: (max+ (chi (E,X))) | (E \/ (XX \ E)) = max+ (chi (E,X)) ;
A15: for x being object st x in dom (max+ (chi (E,X))) holds
0. <= (max+ (chi (E,X))) . x by MESFUNC2:12;
then A16: max+ (chi (E,X)) is nonnegative by SUPINF_2:52;
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 A4, A10, MESFUNC5:81, XBOOLE_1:79;
then A17: integral+ (M,(max+ (chi (E,X)))) = integral+ (M,((max+ (chi (E,X))) | E)) by A14, A11, XXREAL_3:4;

A18: now :: thesis: for x being object st x in dom ((max+ (chi (E,X))) | E) holds
((max+ (chi (E,X))) | E) . x = 1

let x be object ; :: thesis: ( x in dom ((max+ (chi (E,X))) | E) implies ((max+ (chi (E,X))) | E) . x = 1 )
assume A19: x in dom ((max+ (chi (E,X))) | E) ; :: thesis: ((max+ (chi (E,X))) | E) . x = 1
then (chi (E,X)) . x = 1 by A13, FUNCT_3:def 3;
then (max+ (chi (E,X))) . x = 1 by MESFUNC7:23;
hence ((max+ (chi (E,X))) | E) . x = 1 by A19, FUNCT_1:47; :: thesis: verum

end;

then (max+ (chi (E,X))) | E is_simple_func_in S by A13, MESFUNC6:2;
then integral+ (M,(max+ (chi (E,X)))) = integral' (M,((max+ (chi (E,X))) | E)) by A16, A17, MESFUNC5:15, MESFUNC5:77;
then A20: integral+ (M,(max+ (chi (E,X)))) = jj * (M . (dom ((max+ (chi (E,X))) | E))) by A13, A18, MESFUNC5:104;
max+ (chi (E,X)) is E -measurable by A10, MESFUNC1:30;
then (max+ (chi (E,X))) | E is E -measurable by A4, A12, MESFUNC5:42;
then A21: (chi (E,X)) | E is E -measurable by MESFUNC7:23;
(max+ (chi (E,X))) | E is nonnegative by A15, MESFUNC5:15, SUPINF_2:52;
then A22: (chi (E,X)) | E is nonnegative by MESFUNC7:23;
E = dom ((chi (E,X)) | E) by A13, MESFUNC7:23;
then A23: Integral (M,((chi (E,X)) | E)) = integral+ (M,((chi (E,X)) | E)) by A21, A22, MESFUNC5:88;
XX = dom (max- (chi (E,X))) by A3, MESFUNC2:def 3;
then integral+ (M,(max- (chi (E,X)))) = 0 by A3, A9, A1, MESFUNC2:26, MESFUNC5:87;
then Integral (M,(chi (E,X))) = 1 * (M . E) by A13, A20, XXREAL_3:15;
hence Integral (M,(chi (E,X))) = M . E by XXREAL_3:81; :: thesis: Integral (M,((chi (E,X)) | E)) = M . E
(chi (E,X)) | E = (max+ (chi (E,X))) | E by MESFUNC7:23;
hence Integral (M,((chi (E,X)) | E)) = M . E by A13, A17, A20, A23, XXREAL_3:81; :: thesis: verum