let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let M be sigma_Measure of S; :: thesis:
let f be PartFunc of X,ExtREAL ; :: thesis:
assume that
A1: f is_simple_func_in S and
A2: f is nonnegative ; :: thesis:
A3: for x being set st x in dom f holds
0 <= f . x by A2, SUPINF_2:70;

per cases ;

suppose dom f = {} ; :: thesis:

hence 0 <= integral' M,f by Def14; :: thesis:

end;

suppose A4: dom f <> {} ; :: thesis:

then A5: integral' M,f = integral X,S,M,f by Def14;
consider F being Finite_Sep_Sequence of S, a, x being FinSequence of ExtREAL such that
A6: ( F,a are_Re-presentation_of f & dom x = dom F & ( for n being Nat st n in dom x holds
x . n = (a . n) * ((M * F) . n) ) & integral X,S,M,f = Sum x ) by A1, A3, A4, MESFUNC4:4;
for n being Nat st n in dom x holds
0 <= x . n

proof

let n be Nat; :: thesis:
assume A7: n in dom x ; :: thesis:

per cases ;

suppose F . n = {} ; :: thesis:

then M . (F . n) = 0 by VALUED_0:def 19;
then (M * F) . n = 0 by A6, A7, FUNCT_1:23;
then (a . n) * ((M * F) . n) = 0 ;
hence 0 <= x . n by A6, A7; :: thesis:

end;

suppose F . n <> {} ; :: thesis:

then consider v being set such that
A8: v in F . n by XBOOLE_0:def 1;
f . v = a . n by A6, A7, A8, MESFUNC3:def 1;
then A9: 0 <= a . n by A2, SUPINF_2:70;
( F . n in rng F & rng F c= S ) by A6, A7, FUNCT_1:12;
then reconsider Fn = F . n as Element of S ;
0 <= M . Fn by MEASURE1:def 4;
then 0 <= (M * F) . n by A6, A7, FUNCT_1:23;
then 0 <= (a . n) * ((M * F) . n) by A9;
hence 0 <= x . n by A6, A7; :: thesis:

end;

hence 0 <= integral' M,f by A5, A6, Th59; :: thesis:

end;