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:

per cases ;

suppose dom f = {} ; :: thesis:

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

end;

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

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; :: thesis:
assume A10: 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, A10, FUNCT_1:13;
then (a . n) * ((M * F) . n) = 0 ;
hence 0 <= x . n by A7, A10; :: thesis:

end;

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

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:

end;

end;

end;

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

end;

end;