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

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;

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 )

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

then (- 1) (#) ((- f) || A) = f || A by A21, A17, PARTFUN1:5;

hence f is_integrable_on A by A15; :: thesis: verum

end;A4: ( (- f) || A is total & ((- f) || A) | A is bounded )

proof

dom f = dom (- f)
by VALUED_1:8;
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)

for x being object st x in A /\ (dom ((- f) || A)) holds

((- f) || A) . x <= ((- f) || A) . (upper_bound A)

hence ((- f) || A) | A is bounded by A11; :: thesis: verum

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

then A11:
((- f) || A) | A is bounded_below
by RFUNCT_1:71;
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;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

for x being object st x in A /\ (dom ((- f) || A)) holds

((- f) || A) . x <= ((- f) || A) . (upper_bound A)

proof

then
((- f) || A) | A is bounded_above
by RFUNCT_1:70;
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;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

hence ((- f) || A) | A is bounded by A11; :: thesis: verum

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

A = dom (f || A)
by A2, A18, XBOOLE_1:28;
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;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

then (- 1) (#) ((- f) || A) = f || A by A21, A17, PARTFUN1:5;

hence f is_integrable_on A by A15; :: thesis: verum