let A be 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 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: 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 7;
then A7: i in dom D by A6, FINSEQ_3:31;
A8: upper_bound (rng (f | (divset D,i))) >= 0

proof

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

end;

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

end;

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

end;

not dom (upper_sum_set f) is empty by INTEGRA1:def 11;
then ( upper_integral f = lower_bound (rng (upper_sum_set f)) & not rng (upper_sum_set f) is empty ) by INTEGRA1:def 15, RELAT_1:65;
then upper_integral f >= 0 by A3, SEQ_4:60;
hence integral f >= 0 by INTEGRA1:def 18; :: thesis: verum