let a, b be Real; :: thesis: for f being PartFunc of REAL,REAL st a <= b & [.a,b.] c= dom f & f | [.a,b.] is bounded & f | [.a,b.] is nonnegative holds
integral (f,a,b) >= 0
let f be PartFunc of REAL,REAL; :: thesis: ( a <= b & [.a,b.] c= dom f & f | [.a,b.] is bounded & f | [.a,b.] is nonnegative implies integral (f,a,b) >= 0 )
assume that
A1: a <= b and
A2: [.a,b.] c= dom f and
A3: f | [.a,b.] is bounded and
A4: f | [.a,b.] is nonnegative ; :: thesis: integral (f,a,b) >= 0
reconsider A = [.a,b.] as non empty closed_interval Subset of REAL by A1, XXREAL_1:30, MEASURE5:def 3;
dom (f | A) = A by A2, RELAT_1:62;
then reconsider f1 = f | A as Function of A,REAL by FUNCT_2:def 1, RELSET_1:5;
A5: for x being Real st x in A holds
f1 . x >= 0 by A4, MESFUNC6:51;
A6: A = ['a,b'] by A1, INTEGRA5:def 3;
f1 | A is bounded by A3;
then integral f1 >= 0 by A5, INTEGRA2:32;
then integral (f,A) >= 0 by INTEGRA5:def 2;
hence integral (f,a,b) >= 0 by A1, A6, INTEGRA5:def 4; :: thesis: verum