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

then upper_integral f >= 0 by A3, SEQ_4:43;

hence integral f >= 0 by INTEGRA1:def 17; :: thesis: verum

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

( upper_integral f = lower_bound (rng (upper_sum_set f)) & not rng (upper_sum_set f) is empty )
by INTEGRA1:def 14;
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

.= Sum (upper_volume (f,D)) by INTEGRA1:def 8 ;

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

end;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

a =
upper_sum (f,D)
by A4, INTEGRA1:def 10
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

(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;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

A12:
vol (divset (D,i)) >= 0
by INTEGRA1:9;
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;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

(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

.= Sum (upper_volume (f,D)) by INTEGRA1:def 8 ;

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

then upper_integral f >= 0 by A3, SEQ_4:43;

hence integral f >= 0 by INTEGRA1:def 17; :: thesis: verum