let A be non empty closed_interval Subset of REAL; :: thesis: for f being PartFunc of REAL,REAL st f | A is monotone & A c= dom f holds
f is_integrable_on A
let f be PartFunc of REAL,REAL; :: thesis: ( f | A is monotone & A c= dom f implies f is_integrable_on A )
assume that
A1: f | A is monotone and
A2: A c= dom f ; :: thesis: f is_integrable_on A

per cases ( f | A is non-decreasing or f | A is non-increasing ) by A1, RFUNCT_2:def 5;

suppose f | A is non-decreasing ; :: thesis: f is_integrable_on A

hence f is_integrable_on A by A2, Lm1; :: thesis: verum

end;

suppose f | A is non-increasing ; :: thesis: f is_integrable_on A

then A3: ((- 1) (#) f) | A is non-decreasing by RFUNCT_2:35;
A4: ( (- f) || A is total & ((- f) || A) | A is bounded )

proof

consider x being Element of REAL such that
A5: x in A by SUBSET_1:4;
A6: dom ((- f) || A) = (dom (- f)) /\ A by RELAT_1:61
.= (dom f) /\ A by VALUED_1:8
.= A by A2, XBOOLE_1:28 ;
hence (- f) || A is total by PARTFUN1:def 2; :: thesis: ((- f) || A) | A is bounded
( lower_bound A <= x & x <= upper_bound A ) by A5, INTEGRA2:1;
then A7: lower_bound A <= upper_bound A by XXREAL_0:2;
for x being object st x in A /\ (dom ((- f) || A)) holds
((- f) || A) . x >= ((- f) || A) . (lower_bound A)

proof

let x be object ; :: thesis: ( x in A /\ (dom ((- f) || A)) implies ((- f) || A) . x >= ((- f) || A) . (lower_bound A) )
assume x in A /\ (dom ((- f) || A)) ; :: thesis: ((- f) || A) . x >= ((- f) || A) . (lower_bound A)
then reconsider x = x as Element of A ;
A8: ( x >= lower_bound A & (- f) . x = ((- f) | A) . x ) by A6, FUNCT_1:47, INTEGRA2:1;
lower_bound A in A by A7, INTEGRA2:1;
then A9: (- f) . (lower_bound A) = ((- f) | A) . (lower_bound A) by A6, FUNCT_1:47;
A10: A = A /\ (dom f) by A2, XBOOLE_1:28
.= A /\ (dom (- f)) by VALUED_1:8 ;
then lower_bound A in A /\ (dom (- f)) by A7, INTEGRA2:1;
hence ((- f) || A) . x >= ((- f) || A) . (lower_bound A) by A3, A10, A8, A9, RFUNCT_2:24; :: thesis: verum

end;

then A11: ((- f) || A) | A is bounded_below by RFUNCT_1:71;
for x being object st x in A /\ (dom ((- f) || A)) holds
((- f) || A) . x <= ((- f) || A) . (upper_bound A)

proof

let x be object ; :: thesis: ( x in A /\ (dom ((- f) || A)) implies ((- f) || A) . x <= ((- f) || A) . (upper_bound A) )
assume x in A /\ (dom ((- f) || A)) ; :: thesis: ((- f) || A) . x <= ((- f) || A) . (upper_bound A)
then reconsider x = x as Element of A ;
A12: ( x <= upper_bound A & (- f) . x = ((- f) | A) . x ) by A6, FUNCT_1:47, INTEGRA2:1;
upper_bound A in A by A7, INTEGRA2:1;
then A13: (- f) . (upper_bound A) = ((- f) | A) . (upper_bound A) by A6, FUNCT_1:47;
A14: A = A /\ (dom f) by A2, XBOOLE_1:28
.= A /\ (dom (- f)) by VALUED_1:8 ;
then upper_bound A in A /\ (dom (- f)) by A7, INTEGRA2:1;
hence ((- f) || A) . x <= ((- f) || A) . (upper_bound A) by A3, A14, A12, A13, RFUNCT_2:24; :: thesis: verum

end;

then ((- f) || A) | A is bounded_above by RFUNCT_1:70;
hence ((- f) || A) | A is bounded by A11; :: thesis: verum

end;

dom f = dom (- f) by VALUED_1:8;
then - f is_integrable_on A by A2, A3, Lm1;
then (- f) || A is integrable ;
then A15: (- 1) (#) ((- f) || A) is integrable by A4, INTEGRA2:31;
A16: dom ((- f) || A) = (dom (- f)) /\ A by RELAT_1:61
.= (dom f) /\ A by VALUED_1:8
.= A by A2, XBOOLE_1:28 ;
then A17: A = dom ((- 1) (#) ((- f) || A)) by VALUED_1:def 5;
A18: dom (f || A) = (dom f) /\ A by RELAT_1:61;
then A19: dom (f || A) = A by A2, XBOOLE_1:28;
A20: dom ((- 1) (#) ((- f) || A)) = A by A16, VALUED_1:def 5;
A21: for z being Element of A st z in A holds
((- 1) (#) ((- f) || A)) . z = (f || A) . z

proof

let z be Element of A; :: thesis: ( z in A implies ((- 1) (#) ((- f) || A)) . z = (f || A) . z )
assume z in A ; :: thesis: ((- 1) (#) ((- f) || A)) . z = (f || A) . z
((- f) || A) . z = (- f) . z by A16, FUNCT_1:47
.= - (f . z) by VALUED_1:8 ;
then ((- 1) (#) ((- f) || A)) . z = (- 1) * (- (f . z)) by A20, VALUED_1:def 5
.= f . z ;
hence ((- 1) (#) ((- f) || A)) . z = (f || A) . z by A19, FUNCT_1:47; :: thesis: verum

end;

A = dom (f || A) by A2, A18, XBOOLE_1:28;
then (- 1) (#) ((- f) || A) = f || A by A21, A17, PARTFUN1:5;
hence f is_integrable_on A by A15; :: thesis: verum

end;

end;