let X be non empty set ; for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL st f is_simple_func_in S & f is nonnegative holds
0 <= integral' (M,f)
let S be SigmaField of X; for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL st f is_simple_func_in S & f is nonnegative holds
0 <= integral' (M,f)
let M be sigma_Measure of S; for f being PartFunc of X,ExtREAL st f is_simple_func_in S & f is nonnegative holds
0 <= integral' (M,f)
let f be PartFunc of X,ExtREAL; ( f is_simple_func_in S & f is nonnegative implies 0 <= integral' (M,f) )
assume that
A1:
f is_simple_func_in S
and
A2:
f is nonnegative
; 0 <= integral' (M,f)
per cases
( dom f = {} or dom f <> {} )
;
suppose A4:
dom f <> {}
;
0 <= integral' (M,f)then consider F being
Finite_Sep_Sequence of
S,
a,
x being
FinSequence of
ExtREAL such that A5:
F,
a are_Re-presentation_of f
and A6:
dom x = dom F
and A7:
for
n being
Nat st
n in dom x holds
x . n = (a . n) * ((M * F) . n)
and A8:
integral (
M,
f)
= Sum x
by A1, A2, MESFUNC4:4;
A9:
for
n being
Nat st
n in dom x holds
0 <= x . n
proof
let n be
Nat;
( n in dom x implies 0 <= x . n )
assume A10:
n in dom x
;
0 <= x . n
per cases
( F . n = {} or F . n <> {} )
;
suppose
F . n <> {}
;
0 <= x . nthen consider v being
object such that A11:
v in F . n
by XBOOLE_0:def 1;
F . n in rng F
by A6, A10, FUNCT_1:3;
then reconsider Fn =
F . n as
Element of
S ;
0 <= M . Fn
by MEASURE1:def 2;
then A12:
0 <= (M * F) . n
by A6, A10, FUNCT_1:13;
f . v = a . n
by A5, A6, A10, A11, MESFUNC3:def 1;
then
0 <= a . n
by A2, SUPINF_2:51;
then
0 <= (a . n) * ((M * F) . n)
by A12;
hence
0 <= x . n
by A7, A10;
verum end; end;
end;
integral' (
M,
f)
= integral (
M,
f)
by A4, Def14;
hence
0 <= integral' (
M,
f)
by A8, A9, Th53;
verum end; end;