let X be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 0 <= integral' (M,f)

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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 0 <= integral' (M,f)

per cases
( dom f = {} or dom f <> {} )
;

end;

suppose A4:
dom f <> {}
; :: thesis: 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

hence 0 <= integral' (M,f) by A8, A9, Th53; :: thesis: verum

end;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

integral' (M,f) = integral (M,f)
by A4, Def14;
let n be Nat; :: thesis: ( n in dom x implies 0 <= x . n )

assume A10: n in dom x ; :: thesis: 0 <= x . n

end;assume A10: n in dom x ; :: thesis: 0 <= x . n

per cases
( F . n = {} or F . n <> {} )
;

end;

suppose
F . n = {}
; :: thesis: 0 <= x . n

then
M . (F . n) = 0
by VALUED_0:def 19;

then (M * F) . n = 0 by A6, A10, FUNCT_1:13;

then (a . n) * ((M * F) . n) = 0 ;

hence 0 <= x . n by A7, A10; :: thesis: verum

end;then (M * F) . n = 0 by A6, A10, FUNCT_1:13;

then (a . n) * ((M * F) . n) = 0 ;

hence 0 <= x . n by A7, A10; :: thesis: verum

suppose
F . n <> {}
; :: thesis: 0 <= x . n

then 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; :: thesis: verum

end;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; :: thesis: verum

hence 0 <= integral' (M,f) by A8, A9, Th53; :: thesis: verum