let A be closed-interval Subset of REAL ; :: thesis: for f being Function of A,REAL st f | A is bounded & f is integrable & ( for x being Real st x in A holds
f . x >= 0 ) holds
integral f >= 0
let f be Function of A,REAL ; :: thesis: ( f | A is bounded & f is integrable & ( for x being Real st x in A holds
f . x >= 0 ) implies integral f >= 0 )
assume A1: ( f | A is bounded & f is integrable & ( for x being Real st x in A holds
f . x >= 0 ) ) ; :: thesis: integral f >= 0
A2: upper_integral f = lower_bound (rng (upper_sum_set f)) by INTEGRA1:def 15;
not dom (upper_sum_set f) is empty by INTEGRA1:def 11;
then A3: not rng (upper_sum_set f) is empty by RELAT_1:65;
for a being real number st a in rng (upper_sum_set f) holds
a >= 0

proof

let a be real number ; :: thesis: ( a in rng (upper_sum_set f) implies a >= 0 )
assume a in rng (upper_sum_set f) ; :: thesis: a >= 0
then consider D being Element of divs A such that
A4: ( D in dom (upper_sum_set f) & a = (upper_sum_set f) . D ) by PARTFUN1:26;
reconsider D = D as Division of A by INTEGRA1:def 3;
A5: a = upper_sum f,D by A4, INTEGRA1:def 11
.= Sum (upper_volume f,D) by INTEGRA1:def 9 ;
for i being Nat st i in dom (upper_volume f,D) holds
0 <= (upper_volume f,D) . i

proof

let i be Nat; :: thesis: ( i in dom (upper_volume f,D) implies 0 <= (upper_volume f,D) . i )
set r = (upper_volume f,D) . i;
X: len D = len (upper_volume f,D) by INTEGRA1:def 7;
assume i in dom (upper_volume f,D) ; :: thesis: 0 <= (upper_volume f,D) . i
then A6: i in dom D by X, FINSEQ_3:31;
then A7: (upper_volume f,D) . i = (upper_bound (rng (f | (divset D,i)))) * (vol (divset D,i)) by INTEGRA1:def 7;
A8: vol (divset D,i) >= 0 by INTEGRA1:11;
upper_bound (rng (f | (divset D,i))) >= 0

proof

A9: dom (f | (divset D,i)) is non empty Subset of REAL

proof

A10: dom (f | (divset D,i)) = (dom f) /\ (divset D,i) by RELAT_1:90;
dom f = A by FUNCT_2:def 1;
hence dom (f | (divset D,i)) is non empty Subset of REAL by A10, A6, INTEGRA1:10, XBOOLE_1:28; :: thesis: verum

end;

A12: rng (f | (divset D,i)) is bounded_above

proof

f | A is bounded_above by A1;
then rng f is bounded_above by INTEGRA1:15;
hence rng (f | (divset D,i)) is bounded_above by RELAT_1:99, XXREAL_2:43; :: thesis: verum

end;

consider x being Real such that
A13: x in dom (f | (divset D,i)) by A9, SUBSET_1:10;
f . x >= 0 by A1, A13;
then A14: (f | (divset D,i)) . x >= 0 by A13, FUNCT_1:70;
(f | (divset D,i)) . x in rng (f | (divset D,i)) by A13, FUNCT_1:def 5;
hence upper_bound (rng (f | (divset D,i))) >= 0 by A12, A14, SEQ_4:def 4; :: thesis: verum

end;

hence 0 <= (upper_volume f,D) . i by A7, A8; :: thesis: verum

end;

hence a >= 0 by A5, RVSUM_1:114; :: thesis: verum

end;

then upper_integral f >= 0 by A2, A3, SEQ_4:60;
hence integral f >= 0 by INTEGRA1:def 18; :: thesis: verum