let A be non empty closed_interval Subset of REAL; :: thesis: for f being Function of A,REAL st f | A is bounded & ( 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 & ( for x being Real st x in A holds
f . x >= 0 ) implies integral f >= 0 )
assume that
A1: f | A is bounded and
A2: for x being Real st x in A holds
f . x >= 0 ; :: thesis: integral f >= 0
A3: for a being Real st a in rng (upper_sum_set f) holds
a >= 0

proof

let a be Real; :: 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:3;
reconsider D = D as Division of A by INTEGRA1:def 3;
A5: 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;
assume A6: i in dom (upper_volume (f,D)) ; :: thesis: 0 <= (upper_volume (f,D)) . i
len D = len (upper_volume (f,D)) by INTEGRA1:def 6;
then A7: i in dom D by A6, FINSEQ_3:29;
A8: upper_bound (rng (f | (divset (D,i)))) >= 0

proof

rng f is bounded_above by A1, INTEGRA1:13;
then A9: rng (f | (divset (D,i))) is bounded_above by RELAT_1:70, XXREAL_2:43;
( dom (f | (divset (D,i))) = (dom f) /\ (divset (D,i)) & dom f = A ) by FUNCT_2:def 1, RELAT_1:61;
then dom (f | (divset (D,i))) is non empty Subset of REAL by A7, INTEGRA1:8, XBOOLE_1:28;
then consider x being Element of REAL such that
A10: x in dom (f | (divset (D,i))) by SUBSET_1:4;
f . x >= 0 by A2, A10;
then A11: (f | (divset (D,i))) . x >= 0 by A10, FUNCT_1:47;
(f | (divset (D,i))) . x in rng (f | (divset (D,i))) by A10, FUNCT_1:def 3;
hence upper_bound (rng (f | (divset (D,i)))) >= 0 by A9, A11, SEQ_4:def 1; :: thesis: verum

end;

A12: vol (divset (D,i)) >= 0 by INTEGRA1:9;
(upper_volume (f,D)) . i = (upper_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))) by A7, INTEGRA1:def 6;
hence 0 <= (upper_volume (f,D)) . i by A12, A8; :: thesis: verum

end;

a = upper_sum (f,D) by A4, INTEGRA1:def 10
.= Sum (upper_volume (f,D)) by INTEGRA1:def 8 ;
hence a >= 0 by A5, RVSUM_1:84; :: thesis: verum

end;

( upper_integral f = lower_bound (rng (upper_sum_set f)) & not rng (upper_sum_set f) is empty ) by INTEGRA1:def 14;
then upper_integral f >= 0 by A3, SEQ_4:43;
hence integral f >= 0 by INTEGRA1:def 17; :: thesis: verum