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:21;
A2: ( XX = dom (chi E,X) & chi E,X is_measurable_on XX ) by FUNCT_3:def 3, MESFUNC2:32;
then A3: ( XX = dom (max+ (chi E,X)) & max+ (chi E,X) is_measurable_on XX ) by MESFUNC7:23;
set F = XX \ E;
for x being set st x in dom (max+ (chi E,X)) holds
0. <= (max+ (chi E,X)) . x by MESFUNC2:14;
then P1: max+ (chi E,X) is nonnegative by SUPINF_2:71;
then P2: (max+ (chi E,X)) | E is nonnegative by MESFUNC5:21;
X1: 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 A3, P1, MESFUNC5:87, XBOOLE_1:79;
A6: ( XX /\ (XX \ E) = XX \ E & XX /\ E = E ) by XBOOLE_1:28;
then A5: ( dom ((max+ (chi E,X)) | (XX \ E)) = XX \ E & dom ((max+ (chi E,X)) | E) = E ) by A3, RELAT_1:90;
( max+ (chi E,X) is_measurable_on E & max+ (chi E,X) is_measurable_on XX \ E ) by A3, MESFUNC1:34;
then A8: ( (max+ (chi E,X)) | E is_measurable_on E & (max+ (chi E,X)) | (XX \ E) is_measurable_on XX \ E ) by A3, A6, MESFUNC5:48;
E \/ (XX \ E) = XX by A6, XBOOLE_1:51;
then C1: (max+ (chi E,X)) | (E \/ (XX \ E)) = max+ (chi E,X) by A3, RELAT_1:98;

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

end;

then integral+ M,((max+ (chi E,X)) | (XX \ E)) = 0 by A5, A8, MESFUNC5:93;
then X2: integral+ M,(max+ (chi E,X)) = integral+ M,((max+ (chi E,X)) | E) by X1, C1, XXREAL_3:4;

P3: now

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

end;

then (max+ (chi E,X)) | E is_simple_func_in S by A5, MESFUNC6:2;
then integral+ M,(max+ (chi E,X)) = integral' M,((max+ (chi E,X)) | E) by X2, P1, MESFUNC5:21, MESFUNC5:83;
then P8: integral+ M,(max+ (chi E,X)) = (R_EAL 1) * (M . (dom ((max+ (chi E,X)) | E))) by A5, P3, MESFUNC5:110;
P5: ( XX = dom (max- (chi E,X)) & max- (chi E,X) is_measurable_on XX ) by A2, MESFUNC2:28, MESFUNC2:def 3;

now

let x be Element of X; :: thesis: ( x in dom (max- (chi E,X)) implies (max- (chi E,X)) . b₁ = 0 )
assume B1: 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 B1, 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 B1, MESFUNC2:def 3; :: thesis: verum

end;

end;

end;

then QQ: integral+ M,(max- (chi E,X)) = 0 by P5, MESFUNC5:93;
Integral M,(chi E,X) = (R_EAL 1) * (M . E) by P8, A5, QQ, XXREAL_3:15;
hence Integral M,(chi E,X) = M . E by XXREAL_3:92; :: thesis: Integral M,((chi E,X) | E) = M . E
Q1: ( E = dom ((chi E,X) | E) & (chi E,X) | E is_measurable_on E ) by A5, A8, MESFUNC7:23;
Q2: (chi E,X) | E is nonnegative by P2, MESFUNC7:23;
Q3: (chi E,X) | E = (max+ (chi E,X)) | E by MESFUNC7:23;
Integral M,((chi E,X) | E) = integral+ M,((chi E,X) | E) by Q1, Q2, MESFUNC5:94;
hence Integral M,((chi E,X) | E) = M . E by X2, Q3, P8, A5, XXREAL_3:92; :: thesis: verum