let A be non empty closed_interval Subset of REAL; :: thesis: for f being Function of REAL,REAL st f is_integrable_on A & f | A is bounded & integral (f,A) > 0 holds
ex c being Real st
( c in A & f . c > 0 )
let f be Function of REAL,REAL; :: thesis: ( f is_integrable_on A & f | A is bounded & integral (f,A) > 0 implies ex c being Real st
( c in A & f . c > 0 ) )
assume B1: ( f is_integrable_on A & f | A is bounded ) ; :: thesis: ( not integral (f,A) > 0 or ex c being Real st
( c in A & f . c > 0 ) )
assume A1: integral (f,A) > 0 ; :: thesis: ex c being Real st
( c in A & f . c > 0 )
assume A2: for c being Real holds
( not c in A or not f . c > 0 ) ; :: thesis: contradiction
set g = (- 1) (#) f;
ex r being Real st
for y being set st y in dom (((- 1) (#) f) | A) holds
|.((((- 1) (#) f) | A) . y).| < r

proof

consider r being Real such that
C1: for y being set st y in dom (f | A) holds
|.((f | A) . y).| < r by COMSEQ_2:def 3, B1;
take r ; :: thesis: for y being set st y in dom (((- 1) (#) f) | A) holds
|.((((- 1) (#) f) | A) . y).| < r
for y being set st y in dom (((- 1) (#) f) | A) holds
|.((((- 1) (#) f) | A) . y).| < r

proof

let y be set ; :: thesis: ( y in dom (((- 1) (#) f) | A) implies |.((((- 1) (#) f) | A) . y).| < r )
assume C4: y in dom (((- 1) (#) f) | A) ; :: thesis: |.((((- 1) (#) f) | A) . y).| < r
C7: ( dom (f | A) = A & dom (((- 1) (#) f) | A) = A ) by FUNCT_2:def 1;
|.((((- 1) (#) f) | A) . y).| = |.(((- 1) (#) f) . y).| by FUNCT_1:49, C4
.= |.((- 1) * (f . y)).| by VALUED_1:6
.= |.(- (f . y)).|
.= |.(f . y).| by COMPLEX1:52
.= |.((f | A) . y).| by FUNCT_1:49, C4 ;
hence |.((((- 1) (#) f) | A) . y).| < r by C1, C4, C7; :: thesis: verum

end;

hence for y being set st y in dom (((- 1) (#) f) | A) holds
|.((((- 1) (#) f) | A) . y).| < r ; :: thesis: verum

end;

then A4: (((- 1) (#) f) | A) | A is bounded by COMSEQ_2:def 3;
for x being Real st x in A holds
0 <= (((- 1) (#) f) | A) . x

proof

let x be Real; :: thesis: ( x in A implies 0 <= (((- 1) (#) f) | A) . x )
assume C2: x in A ; :: thesis: 0 <= (((- 1) (#) f) | A) . x
C3: f . x <= 0 by A2, C2;
(((- 1) (#) f) | A) . x = ((- 1) (#) f) . x by FUNCT_1:49, C2
.= (- 1) * (f . x) by VALUED_1:6 ;
hence 0 <= (((- 1) (#) f) | A) . x by C3; :: thesis: verum

end;

then A6: 0 <= integral (((- 1) (#) f) | A) by A4, INTEGRA2:32;
reconsider f = f as PartFunc of REAL,REAL ;
dom f = REAL by FUNCT_2:def 1;
then ( A c= dom f & f is_integrable_on A & f | A is bounded ) by B1;
then integral (((- 1) (#) f),A) = (- 1) * (integral (f,A)) by INTEGRA6:9;
hence contradiction by A1, A6, INTEGRA5:def 2; :: thesis: verum