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:
A3: for a being Real st a in rng () holds
a >= 0
proof
let a be Real; :: thesis: ( a in rng () implies a >= 0 )
assume a in rng () ; :: thesis: a >= 0
then consider D being Element of divs A such that
A4: ( D in dom () & a = () . 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 ;
A8: upper_bound (rng (f | (divset (D,i)))) >= 0
proof
rng f is bounded_above by ;
then A9: rng (f | (divset (D,i))) is bounded_above by ;
( dom (f | (divset (D,i))) = (dom f) /\ (divset (D,i)) & dom f = A ) by ;
then dom (f | (divset (D,i))) is non empty Subset of REAL by ;
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 ;
then A11: (f | (divset (D,i))) . x >= 0 by ;
(f | (divset (D,i))) . x in rng (f | (divset (D,i))) by ;
hence upper_bound (rng (f | (divset (D,i)))) >= 0 by ; :: 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 ;
hence 0 <= (upper_volume (f,D)) . i by ; :: thesis: verum
end;
a = upper_sum (f,D) by
.= Sum (upper_volume (f,D)) by INTEGRA1:def 8 ;
hence a >= 0 by ; :: thesis: verum
end;
( upper_integral f = lower_bound (rng ()) & not rng () is empty ) by INTEGRA1:def 14;
then upper_integral f >= 0 by ;
hence integral f >= 0 by INTEGRA1:def 17; :: thesis: verum