let A be non empty closed_interval Subset of REAL; :: thesis: for f being Function of A,REAL st f | A is bounded & f is integrable holds
max- f is integrable
let f be Function of A,REAL; :: thesis: ( f | A is bounded & f is integrable implies max- f is integrable )
assume that
A1: f | A is bounded and
A2: f is integrable ; :: thesis: max- f is integrable
A3: (- f) | A is bounded by A1, RFUNCT_1:82;
(- 1) (#) f is integrable by A1, A2, INTEGRA2:31;
then max+ (- f) is integrable by A3, Th20;
hence max- f is integrable by Th21; :: thesis: verum