let X be non empty set ; 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; 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; 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; ( 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:7;
set F = XX \ E;
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:61;
A10:
chi (E,X) is XX -measurable
by MESFUNC2:29;
then A11:
max+ (chi (E,X)) is XX -measurable
by Th23;
then
max+ (chi (E,X)) is XX \ E -measurable
by MESFUNC1:30;
then A12:
integral+ (M,((max+ (chi (E,X))) | (XX \ E))) = 0
by A5, A6, A7, A8, MESFUNC5:42, MESFUNC5:87;
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:26, MESFUNC5:87;
A14:
XX /\ E = E
by XBOOLE_1:28;
then A15:
dom ((max+ (chi (E,X))) | E) = E
by A5, RELAT_1:61;
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:69;
A17:
for x being object st x in dom (max+ (chi (E,X))) holds
0. <= (max+ (chi (E,X))) . x
by MESFUNC2:12;
then A18:
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 A5, A11, MESFUNC5:81, XBOOLE_1:79;
then A19:
integral+ (M,(max+ (chi (E,X)))) = integral+ (M,((max+ (chi (E,X))) | E))
by A16, A12, XXREAL_3:4;
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:15, MESFUNC5:77;
then A22:
integral+ (M,(max+ (chi (E,X)))) = jj * (M . (dom ((max+ (chi (E,X))) | E)))
by A15, A20, MESFUNC5:104;
max+ (chi (E,X)) is E -measurable
by A11, MESFUNC1:30;
then
(max+ (chi (E,X))) | E is E -measurable
by A5, A14, MESFUNC5:42;
then A23:
(chi (E,X)) | E is E -measurable
by Th23;
(max+ (chi (E,X))) | E is nonnegative
by A17, MESFUNC5:15, SUPINF_2:52;
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:88;
assume
M . E < +infty
; ( 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:81;
hence
chi (E,X) is_integrable_on M
by A4, A10, A13; ( Integral (M,(chi (E,X))) = M . E & Integral (M,((chi (E,X)) | E)) = M . E )
Integral (M,(chi (E,X))) = 1 * (M . E)
by A15, A22, A13, XXREAL_3:15;
hence
Integral (M,(chi (E,X))) = M . E
by XXREAL_3:81; 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:81; verum