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
for er being ExtReal holds Integral (M,(chi (er,E,X))) = er * (M . E)
let S be SigmaField of X; for M being sigma_Measure of S
for E being Element of S
for er being ExtReal holds Integral (M,(chi (er,E,X))) = er * (M . E)
let M be sigma_Measure of S; for E being Element of S
for er being ExtReal holds Integral (M,(chi (er,E,X))) = er * (M . E)
let E be Element of S; for er being ExtReal holds Integral (M,(chi (er,E,X))) = er * (M . E)
let er be ExtReal; Integral (M,(chi (er,E,X))) = er * (M . E)
reconsider XX = X as Element of S by MEASURE1:7;
per cases
( er = +infty or er = -infty or ( er <> +infty & er <> -infty ) )
;
suppose a6:
er = -infty
;
Integral (M,(chi (er,E,X))) = er * (M . E)then a7:
chi (
er,
E,
X)
= - (Xchi (E,X))
by Th2;
a10:
dom (Xchi (E,X)) = XX
by FUNCT_2:def 1;
W:
Xchi (
E,
X) is
XX -measurable
by MEASUR10:32;
per cases
( M . E <> 0 or M . E = 0 )
;
suppose a8:
M . E <> 0
;
Integral (M,(chi (er,E,X))) = er * (M . E)then a9:
M . E > 0
by MEASURE1:def 2;
thus Integral (
M,
(chi (er,E,X))) =
- (Integral (M,(Xchi (E,X))))
by a10, a7, MESFUN11:52, W
.=
- +infty
by a8, MEASUR10:33
.=
er * (M . E)
by a6, a9, XXREAL_3:def 5, XXREAL_3:6
;
verum end; end; end; suppose
(
er <> +infty &
er <> -infty )
;
Integral (M,(chi (er,E,X))) = er * (M . E)then
er in REAL
by XXREAL_0:14;
then reconsider r =
er as
Real ;
a14:
chi (
E,
X)
is_simple_func_in S
by Th12;
chi (
er,
E,
X)
= r (#) (chi (E,X))
by Th1;
hence Integral (
M,
(chi (er,E,X))) =
r * (integral' (M,(chi (E,X))))
by Th12, MESFUN11:59
.=
r * (Integral (M,(chi (E,X))))
by a14, MESFUNC5:89
.=
er * (M . E)
by MESFUNC9:14
;
verum end; end;