let A be 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
max+ f is total by Th13;
then A3: max+ f is Function of A,REAL ;
f | A is bounded_above by A1;
then ( (max+ f) | A is bounded_above & (max+ f) | A is bounded_below ) by Th14, Th15;
then A4: (max+ f) | A is bounded ;
for T being DivSequence of A st delta T is convergent & lim (delta T) = 0 holds
(lim (upper_sum (max+ f),T)) - (lim (lower_sum (max+ f),T)) = 0

proof

let T be DivSequence of A; :: thesis: ( delta T is convergent & lim (delta T) = 0 implies (lim (upper_sum (max+ f),T)) - (lim (lower_sum (max+ f),T)) = 0 )
assume that
A5: delta T is convergent and
A6: lim (delta T) = 0 ; :: thesis: (lim (upper_sum (max+ f),T)) - (lim (lower_sum (max+ f),T)) = 0
A7: ( upper_sum (max+ f),T is convergent & lower_sum (max+ f),T is convergent ) by A3, A4, A5, A6, Th8, Th9;
A8: ( upper_sum f,T is convergent & lower_sum f,T is convergent ) by A1, A5, A6, Th8, Th9;
A9: (lim (upper_sum f,T)) - (lim (lower_sum f,T)) = 0 by A1, A2, A5, A6, Th12;
A10: (upper_sum f,T) - (lower_sum f,T) is convergent by A8, SEQ_2:25;
reconsider osc = (upper_sum f,T) - (lower_sum f,T) as Real_Sequence ;
reconsider osc1 = (upper_sum (max+ f),T) - (lower_sum (max+ f),T) as Real_Sequence ;
A11: lim ((upper_sum f,T) - (lower_sum f,T)) = 0 by A8, A9, SEQ_2:26;
A12: for a being real number st 0 < a holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((osc1 . m) - 0 ) < a

proof

let a be real number ; :: thesis: ( 0 < a implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((osc1 . m) - 0 ) < a )
assume 0 < a ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((osc1 . m) - 0 ) < a
then consider n being Element of NAT such that
A13: for m being Element of NAT st n <= m holds
abs ((osc . m) - 0 ) < a by A10, A11, SEQ_2:def 7;
for m being Element of NAT st n <= m holds
abs ((osc1 . m) - 0 ) < a

proof

let m be Element of NAT ; :: thesis: ( n <= m implies abs ((osc1 . m) - 0 ) < a )
assume n <= m ; :: thesis: abs ((osc1 . m) - 0 ) < a
then A14: abs ((osc . m) - 0 ) < a by A13;
reconsider D = T . m as Division of A ;
A15: osc . m = ((upper_sum f,T) . m) + ((- (lower_sum f,T)) . m) by SEQ_1:11
.= ((upper_sum f,T) . m) + (- ((lower_sum f,T) . m)) by SEQ_1:14
.= ((upper_sum f,T) . m) - ((lower_sum f,T) . m)
.= (upper_sum f,(T . m)) - ((lower_sum f,T) . m) by INTEGRA2:def 4
.= (upper_sum f,(T . m)) - (lower_sum f,(T . m)) by INTEGRA2:def 5
.= (Sum (upper_volume f,D)) - (lower_sum f,(T . m)) by INTEGRA1:def 9
.= (Sum (upper_volume f,D)) - (Sum (lower_volume f,D)) by INTEGRA1:def 10 ;
len (upper_volume f,D) = len D by INTEGRA1:def 7;
then reconsider UV = upper_volume f,D as Element of (len D) -tuples_on REAL by CATALG_1:5;
len (lower_volume f,D) = len D by INTEGRA1:def 8;
then reconsider LV = lower_volume f,D as Element of (len D) -tuples_on REAL by CATALG_1:5;
A16: osc . m = Sum (UV - LV) by A15, RVSUM_1:120;
A17: osc1 . m = ((upper_sum (max+ f),T) . m) + ((- (lower_sum (max+ f),T)) . m) by SEQ_1:11
.= ((upper_sum (max+ f),T) . m) + (- ((lower_sum (max+ f),T) . m)) by SEQ_1:14
.= ((upper_sum (max+ f),T) . m) - ((lower_sum (max+ f),T) . m)
.= (upper_sum (max+ f),(T . m)) - ((lower_sum (max+ f),T) . m) by INTEGRA2:def 4
.= (upper_sum (max+ f),(T . m)) - (lower_sum (max+ f),(T . m)) by INTEGRA2:def 5
.= (Sum (upper_volume (max+ f),D)) - (lower_sum (max+ f),(T . m)) by INTEGRA1:def 9
.= (Sum (upper_volume (max+ f),D)) - (Sum (lower_volume (max+ f),D)) by INTEGRA1:def 10 ;
len (upper_volume (max+ f),D) = len D by INTEGRA1:def 7;
then reconsider UV1 = upper_volume (max+ f),D as Element of (len D) -tuples_on REAL by CATALG_1:5;
len (lower_volume (max+ f),D) = len D by INTEGRA1:def 8;
then reconsider LV1 = lower_volume (max+ f),D as Element of (len D) -tuples_on REAL by CATALG_1:5;
A18: osc1 . m = Sum (UV1 - LV1) by A17, RVSUM_1:120;
for j being Nat st j in Seg (len D) holds
(UV1 - LV1) . j <= (UV - LV) . j

proof

let j be Nat; :: thesis: ( j in Seg (len D) implies (UV1 - LV1) . j <= (UV - LV) . j )
assume A19: j in Seg (len D) ; :: thesis: (UV1 - LV1) . j <= (UV - LV) . j
then B19: j in dom D by FINSEQ_1:def 3;
set x = (UV1 - LV1) . j;
set y = (UV - LV) . j;
A20: UV1 . j = (upper_bound (rng ((max+ f) | (divset D,j)))) * (vol (divset D,j)) by B19, INTEGRA1:def 7;
LV1 . j = (lower_bound (rng ((max+ f) | (divset D,j)))) * (vol (divset D,j)) by B19, INTEGRA1:def 8;
then A21: (UV1 - LV1) . j = ((upper_bound (rng ((max+ f) | (divset D,j)))) * (vol (divset D,j))) - ((lower_bound (rng ((max+ f) | (divset D,j)))) * (vol (divset D,j))) by A20, RVSUM_1:48
.= ((upper_bound (rng ((max+ f) | (divset D,j)))) - (lower_bound (rng ((max+ f) | (divset D,j))))) * (vol (divset D,j)) ;
A22: UV . j = (upper_bound (rng (f | (divset D,j)))) * (vol (divset D,j)) by B19, INTEGRA1:def 7;
LV . j = (lower_bound (rng (f | (divset D,j)))) * (vol (divset D,j)) by B19, INTEGRA1:def 8;
then A23: (UV - LV) . j = ((upper_bound (rng (f | (divset D,j)))) * (vol (divset D,j))) - ((lower_bound (rng (f | (divset D,j)))) * (vol (divset D,j))) by A22, RVSUM_1:48
.= ((upper_bound (rng (f | (divset D,j)))) - (lower_bound (rng (f | (divset D,j))))) * (vol (divset D,j)) ;
A24: upper_bound (rng (f | (divset D,j))) >= lower_bound (rng (f | (divset D,j)))

proof

( rng (f | (divset D,j)) is bounded & ex r being Real st r in rng (f | (divset D,j)) )

proof

consider r being Real such that
A25: r in divset D,j by SUBSET_1:10;
j in dom D by A19, FINSEQ_1:def 3;
then divset D,j c= A by INTEGRA1:10;
then r in A by A25;
then r in dom f by FUNCT_2:def 1;
then A26: f . r in rng (f | (divset D,j)) by A25, FUNCT_1:73;
( f | A is bounded_above & f | A is bounded_below ) by A1;
then ( rng f is bounded_above & rng f is bounded_below ) by INTEGRA1:13, INTEGRA1:15;
then rng f is bounded ;
hence rng (f | (divset D,j)) is bounded by RELAT_1:99, XXREAL_2:45; :: thesis: ex r being Real st r in rng (f | (divset D,j))
thus ex r being Real st r in rng (f | (divset D,j)) by A26; :: thesis: verum

end;

hence upper_bound (rng (f | (divset D,j))) >= lower_bound (rng (f | (divset D,j))) by SEQ_4:24; :: thesis: verum

end;

A27: (upper_bound (rng (f | (divset D,j)))) - (lower_bound (rng (f | (divset D,j)))) >= (upper_bound (rng ((max+ f) | (divset D,j)))) - (lower_bound (rng ((max+ f) | (divset D,j))))

proof

set M = upper_bound (rng (f | (divset D,j)));
set m = lower_bound (rng (f | (divset D,j)));
set M1 = upper_bound (rng ((max+ f) | (divset D,j)));
set m1 = lower_bound (rng ((max+ f) | (divset D,j)));
A28: dom (f | (divset D,j)) = (dom f) /\ (divset D,j) by RELAT_1:90;
A29: dom f = A by FUNCT_2:def 1;
A30: dom (f | (divset D,j)) = A /\ (divset D,j) by A28, FUNCT_2:def 1;
A31: j in dom D by A19, FINSEQ_1:def 3;
then dom (f | (divset D,j)) <> {} by A30, INTEGRA1:10, XBOOLE_1:28;
then A32: rng (f | (divset D,j)) <> {} by RELAT_1:65;
A33: ( f | A is bounded_above & f | A is bounded_below ) by A1;
then A34: ( rng (f | (divset D,j)) is bounded_above & rng (f | (divset D,j)) is bounded_below ) by Th18, Th19;
dom f = dom (max+ f) by RFUNCT_3:def 10;
then dom ((max+ f) | (divset D,j)) = A /\ (divset D,j) by A29, RELAT_1:90;
then dom ((max+ f) | (divset D,j)) <> {} by A31, INTEGRA1:10, XBOOLE_1:28;
then A35: rng ((max+ f) | (divset D,j)) <> {} by RELAT_1:65;
( (max+ f) | A is bounded_above & (max+ f) | A is bounded_below ) by A33, Th14, Th15;
then A36: ( rng ((max+ f) | (divset D,j)) is bounded_above & rng ((max+ f) | (divset D,j)) is bounded_below ) by Th18, Th19;

now

per cases ( ( upper_bound (rng (f | (divset D,j))) > 0 & lower_bound (rng (f | (divset D,j))) >= 0 ) or ( upper_bound (rng (f | (divset D,j))) > 0 & lower_bound (rng (f | (divset D,j))) <= 0 ) or ( upper_bound (rng (f | (divset D,j))) <= 0 & lower_bound (rng (f | (divset D,j))) <= 0 ) ) by A24;

suppose A37: ( upper_bound (rng (f | (divset D,j))) > 0 & lower_bound (rng (f | (divset D,j))) >= 0 ) ; :: thesis: (upper_bound (rng (f | (divset D,j)))) - (lower_bound (rng (f | (divset D,j)))) >= (upper_bound (rng ((max+ f) | (divset D,j)))) - (lower_bound (rng ((max+ f) | (divset D,j))))

( upper_bound (rng ((max+ f) | (divset D,j))) = upper_bound (rng (f | (divset D,j))) & lower_bound (rng ((max+ f) | (divset D,j))) = lower_bound (rng (f | (divset D,j))) )

proof

( ( for r being real number st r in rng ((max+ f) | (divset D,j)) holds
r <= upper_bound (rng (f | (divset D,j))) ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in rng ((max+ f) | (divset D,j)) & (upper_bound (rng (f | (divset D,j)))) - s < r ) ) )

proof

A38: for r being real number st r in rng ((max+ f) | (divset D,j)) holds
r <= upper_bound (rng (f | (divset D,j)))

proof

let r be real number ; :: thesis: ( r in rng ((max+ f) | (divset D,j)) implies r <= upper_bound (rng (f | (divset D,j))) )
assume r in rng ((max+ f) | (divset D,j)) ; :: thesis: r <= upper_bound (rng (f | (divset D,j)))
then consider x being Element of A such that
A39: ( x in dom ((max+ f) | (divset D,j)) & r = ((max+ f) | (divset D,j)) . x ) by PARTFUN1:26;
A40: r = (max+ (f | (divset D,j))) . x by A39, RFUNCT_3:47;
A41: x in dom (max+ (f | (divset D,j))) by A39, RFUNCT_3:47;
then A42: x in dom (f | (divset D,j)) by RFUNCT_3:def 10;

now

per cases ( r = 0 or r > 0 ) by A40, RFUNCT_3:40;

suppose r = 0 ; :: thesis: r <= upper_bound (rng (f | (divset D,j)))

hence r <= upper_bound (rng (f | (divset D,j))) by A37; :: thesis: verum

end;

suppose A43: r > 0 ; :: thesis: r <= upper_bound (rng (f | (divset D,j)))

r = max+ ((f | (divset D,j)) . x) by A40, A41, RFUNCT_3:def 10;
then r = max ((f | (divset D,j)) . x),0 by RFUNCT_3:def 1;
then r = (f | (divset D,j)) . x by A43, XXREAL_0:def 10;
then r in rng (f | (divset D,j)) by A42, FUNCT_1:def 5;
hence r <= upper_bound (rng (f | (divset D,j))) by A34, SEQ_4:def 4; :: thesis: verum

end;

end;

end;

hence r <= upper_bound (rng (f | (divset D,j))) ; :: thesis: verum

end;

for s being real number st 0 < s holds
ex r being real number st
( r in rng ((max+ f) | (divset D,j)) & (upper_bound (rng (f | (divset D,j)))) - s < r )

proof

let s be real number ; :: thesis: ( 0 < s implies ex r being real number st
( r in rng ((max+ f) | (divset D,j)) & (upper_bound (rng (f | (divset D,j)))) - s < r ) )
assume 0 < s ; :: thesis: ex r being real number st
( r in rng ((max+ f) | (divset D,j)) & (upper_bound (rng (f | (divset D,j)))) - s < r )
then consider r being real number such that
A44: ( r in rng (f | (divset D,j)) & (upper_bound (rng (f | (divset D,j)))) - s < r ) by A32, A34, SEQ_4:def 4;
r in rng ((max+ f) | (divset D,j))

proof

consider x being Element of A such that
A45: ( x in dom (f | (divset D,j)) & r = (f | (divset D,j)) . x ) by A44, PARTFUN1:26;
A46: r >= lower_bound (rng (f | (divset D,j))) by A34, A44, SEQ_4:def 5;
reconsider r1 = r as Real by XREAL_0:def 1;
A47: x in dom (max+ (f | (divset D,j))) by A45, RFUNCT_3:def 10;
then (max+ (f | (divset D,j))) . x = max+ r1 by A45, RFUNCT_3:def 10
.= max r,0 by RFUNCT_3:def 1
.= r by A37, A46, XXREAL_0:def 10 ;
then r in rng (max+ (f | (divset D,j))) by A47, FUNCT_1:def 5;
hence r in rng ((max+ f) | (divset D,j)) by RFUNCT_3:47; :: thesis: verum

end;

hence ex r being real number st
( r in rng ((max+ f) | (divset D,j)) & (upper_bound (rng (f | (divset D,j)))) - s < r ) by A44; :: thesis: verum

end;

hence ( ( for r being real number st r in rng ((max+ f) | (divset D,j)) holds
r <= upper_bound (rng (f | (divset D,j))) ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in rng ((max+ f) | (divset D,j)) & (upper_bound (rng (f | (divset D,j)))) - s < r ) ) ) by A38; :: thesis: verum

end;

hence upper_bound (rng ((max+ f) | (divset D,j))) = upper_bound (rng (f | (divset D,j))) by A35, A36, SEQ_4:def 4; :: thesis: lower_bound (rng ((max+ f) | (divset D,j))) = lower_bound (rng (f | (divset D,j)))
( ( for r being real number st r in rng ((max+ f) | (divset D,j)) holds
lower_bound (rng (f | (divset D,j))) <= r ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in rng ((max+ f) | (divset D,j)) & r < (lower_bound (rng (f | (divset D,j)))) + s ) ) )

proof

A48: for r being real number st r in rng ((max+ f) | (divset D,j)) holds
lower_bound (rng (f | (divset D,j))) <= r

proof

let r be real number ; :: thesis: ( r in rng ((max+ f) | (divset D,j)) implies lower_bound (rng (f | (divset D,j))) <= r )
assume r in rng ((max+ f) | (divset D,j)) ; :: thesis: lower_bound (rng (f | (divset D,j))) <= r
then consider x being Element of A such that
A49: ( x in dom ((max+ f) | (divset D,j)) & r = ((max+ f) | (divset D,j)) . x ) by PARTFUN1:26;
A50: x in dom (max+ (f | (divset D,j))) by A49, RFUNCT_3:47;
A51: r = (max+ (f | (divset D,j))) . x by A49, RFUNCT_3:47
.= max+ ((f | (divset D,j)) . x) by A50, RFUNCT_3:def 10
.= max ((f | (divset D,j)) . x),0 by RFUNCT_3:def 1 ;
x in dom (max+ (f | (divset D,j))) by A49, RFUNCT_3:47;
then x in dom (f | (divset D,j)) by RFUNCT_3:def 10;
then (f | (divset D,j)) . x in rng (f | (divset D,j)) by FUNCT_1:def 5;
then (f | (divset D,j)) . x >= lower_bound (rng (f | (divset D,j))) by A34, SEQ_4:def 5;
hence lower_bound (rng (f | (divset D,j))) <= r by A37, A51, XXREAL_0:def 10; :: thesis: verum

end;

for s being real number st 0 < s holds
ex r being real number st
( r in rng ((max+ f) | (divset D,j)) & r < (lower_bound (rng (f | (divset D,j)))) + s )

proof

let s be real number ; :: thesis: ( 0 < s implies ex r being real number st
( r in rng ((max+ f) | (divset D,j)) & r < (lower_bound (rng (f | (divset D,j)))) + s ) )
assume 0 < s ; :: thesis: ex r being real number st
( r in rng ((max+ f) | (divset D,j)) & r < (lower_bound (rng (f | (divset D,j)))) + s )
then consider r being real number such that
A52: ( r in rng (f | (divset D,j)) & r < (lower_bound (rng (f | (divset D,j)))) + s ) by A32, A34, SEQ_4:def 5;
reconsider r = r as Real by XREAL_0:def 1;
r in rng ((max+ f) | (divset D,j))

proof

consider x being Element of A such that
A53: ( x in dom (f | (divset D,j)) & r = (f | (divset D,j)) . x ) by A52, PARTFUN1:26;
A54: r >= lower_bound (rng (f | (divset D,j))) by A34, A52, SEQ_4:def 5;
A55: x in dom (max+ (f | (divset D,j))) by A53, RFUNCT_3:def 10;
then (max+ (f | (divset D,j))) . x = max+ r by A53, RFUNCT_3:def 10
.= max r,0 by RFUNCT_3:def 1
.= r by A37, A54, XXREAL_0:def 10 ;
then r in rng (max+ (f | (divset D,j))) by A55, FUNCT_1:def 5;
hence r in rng ((max+ f) | (divset D,j)) by RFUNCT_3:47; :: thesis: verum

end;

hence ex r being real number st
( r in rng ((max+ f) | (divset D,j)) & r < (lower_bound (rng (f | (divset D,j)))) + s ) by A52; :: thesis: verum

end;

hence ( ( for r being real number st r in rng ((max+ f) | (divset D,j)) holds
lower_bound (rng (f | (divset D,j))) <= r ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in rng ((max+ f) | (divset D,j)) & r < (lower_bound (rng (f | (divset D,j)))) + s ) ) ) by A48; :: thesis: verum

end;

hence lower_bound (rng ((max+ f) | (divset D,j))) = lower_bound (rng (f | (divset D,j))) by A35, A36, SEQ_4:def 5; :: thesis: verum

end;

hence (upper_bound (rng (f | (divset D,j)))) - (lower_bound (rng (f | (divset D,j)))) >= (upper_bound (rng ((max+ f) | (divset D,j)))) - (lower_bound (rng ((max+ f) | (divset D,j)))) ; :: thesis: verum

end;

suppose A56: ( upper_bound (rng (f | (divset D,j))) > 0 & lower_bound (rng (f | (divset D,j))) <= 0 ) ; :: thesis: (upper_bound (rng (f | (divset D,j)))) - (lower_bound (rng (f | (divset D,j)))) >= (upper_bound (rng ((max+ f) | (divset D,j)))) - (lower_bound (rng ((max+ f) | (divset D,j))))

( upper_bound (rng ((max+ f) | (divset D,j))) = upper_bound (rng (f | (divset D,j))) & lower_bound (rng ((max+ f) | (divset D,j))) = 0 )

proof

( ( for r being real number st r in rng ((max+ f) | (divset D,j)) holds
r <= upper_bound (rng (f | (divset D,j))) ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in rng ((max+ f) | (divset D,j)) & (upper_bound (rng (f | (divset D,j)))) - s < r ) ) )

proof

A57: for r being Real st r in rng ((max+ f) | (divset D,j)) holds
r <= upper_bound (rng (f | (divset D,j)))

proof

let r be Real; :: thesis: ( r in rng ((max+ f) | (divset D,j)) implies r <= upper_bound (rng (f | (divset D,j))) )
assume r in rng ((max+ f) | (divset D,j)) ; :: thesis: r <= upper_bound (rng (f | (divset D,j)))
then consider x being Element of A such that
A58: ( x in dom ((max+ f) | (divset D,j)) & r = ((max+ f) | (divset D,j)) . x ) by PARTFUN1:26;
A59: r = (max+ (f | (divset D,j))) . x by A58, RFUNCT_3:47;
A60: x in dom (max+ (f | (divset D,j))) by A58, RFUNCT_3:47;
then A61: x in dom (f | (divset D,j)) by RFUNCT_3:def 10;

now

per cases ( r = 0 or r > 0 ) by A59, RFUNCT_3:40;

suppose r = 0 ; :: thesis: r <= upper_bound (rng (f | (divset D,j)))

hence r <= upper_bound (rng (f | (divset D,j))) by A56; :: thesis: verum

end;

suppose A62: r > 0 ; :: thesis: r <= upper_bound (rng (f | (divset D,j)))

r = max+ ((f | (divset D,j)) . x) by A59, A60, RFUNCT_3:def 10;
then r = max ((f | (divset D,j)) . x),0 by RFUNCT_3:def 1;
then r = (f | (divset D,j)) . x by A62, XXREAL_0:def 10;
then r in rng (f | (divset D,j)) by A61, FUNCT_1:def 5;
hence r <= upper_bound (rng (f | (divset D,j))) by A34, SEQ_4:def 4; :: thesis: verum

end;

end;

end;

hence r <= upper_bound (rng (f | (divset D,j))) ; :: thesis: verum

end;

for s being real number st 0 < s holds
ex r being real number st
( r in rng ((max+ f) | (divset D,j)) & (upper_bound (rng (f | (divset D,j)))) - s < r )

proof

assume ex s being real number st
( 0 < s & ( for r being real number holds
( not r in rng ((max+ f) | (divset D,j)) or not (upper_bound (rng (f | (divset D,j)))) - s < r ) ) ) ; :: thesis: contradiction
then consider s being real number such that
A63: ( s > 0 & ( for r being real number st r in rng ((max+ f) | (divset D,j)) holds
(upper_bound (rng (f | (divset D,j)))) - s >= r ) ) ;
consider r1 being real number such that
A64: ( r1 in rng (f | (divset D,j)) & (upper_bound (rng (f | (divset D,j)))) - s < r1 ) by A32, A34, A63, SEQ_4:def 4;
consider x being Element of A such that
A65: ( x in dom (f | (divset D,j)) & r1 = (f | (divset D,j)) . x ) by A64, PARTFUN1:26;
A66: x in dom (max+ (f | (divset D,j))) by A65, RFUNCT_3:def 10;
(max+ (f | (divset D,j))) . x >= 0 by RFUNCT_3:40;
then A67: ((max+ f) | (divset D,j)) . x >= 0 by RFUNCT_3:47;
x in dom ((max+ f) | (divset D,j)) by A66, RFUNCT_3:47;
then A68: ((max+ f) | (divset D,j)) . x in rng ((max+ f) | (divset D,j)) by FUNCT_1:def 5;
then A69: (upper_bound (rng (f | (divset D,j)))) - s >= 0 by A63, A67;
((max+ f) | (divset D,j)) . x = (max+ (f | (divset D,j))) . x by RFUNCT_3:47
.= max+ ((f | (divset D,j)) . x) by A66, RFUNCT_3:def 10
.= max r1,0 by A65, RFUNCT_3:def 1
.= r1 by A64, A69, XXREAL_0:def 10 ;
hence contradiction by A63, A64, A68; :: thesis: verum

end;

hence ( ( for r being real number st r in rng ((max+ f) | (divset D,j)) holds
r <= upper_bound (rng (f | (divset D,j))) ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in rng ((max+ f) | (divset D,j)) & (upper_bound (rng (f | (divset D,j)))) - s < r ) ) ) by A57; :: thesis: verum

end;

hence upper_bound (rng ((max+ f) | (divset D,j))) = upper_bound (rng (f | (divset D,j))) by A35, A36, SEQ_4:def 4; :: thesis: lower_bound (rng ((max+ f) | (divset D,j))) = 0
( ( for r being real number st r in rng ((max+ f) | (divset D,j)) holds
0 <= r ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in rng ((max+ f) | (divset D,j)) & r < 0 + s ) ) )

proof

A70: for r being real number st r in rng ((max+ f) | (divset D,j)) holds
0 <= r

proof

let r be real number ; :: thesis: ( r in rng ((max+ f) | (divset D,j)) implies 0 <= r )
assume r in rng ((max+ f) | (divset D,j)) ; :: thesis: 0 <= r
then r in rng (max+ (f | (divset D,j))) by RFUNCT_3:47;
then consider x being Element of A such that
A71: ( x in dom (max+ (f | (divset D,j))) & r = (max+ (f | (divset D,j))) . x ) by PARTFUN1:26;
thus 0 <= r by A71, RFUNCT_3:40; :: thesis: verum

end;

for s being real number st 0 < s holds
ex r being real number st
( r in rng ((max+ f) | (divset D,j)) & r < 0 + s )

proof

let s be real number ; :: thesis: ( 0 < s implies ex r being real number st
( r in rng ((max+ f) | (divset D,j)) & r < 0 + s ) )
assume A72: s > 0 ; :: thesis: ex r being real number st
( r in rng ((max+ f) | (divset D,j)) & r < 0 + s )
then consider r being real number such that
A73: ( r in rng (f | (divset D,j)) & r < (lower_bound (rng (f | (divset D,j)))) + s ) by A32, A34, SEQ_4:def 5;
A74: r - s < lower_bound (rng (f | (divset D,j))) by A73, XREAL_1:21;
consider x being Element of A such that
A75: ( x in dom (f | (divset D,j)) & r = (f | (divset D,j)) . x ) by A73, PARTFUN1:26;
A76: x in dom (max+ (f | (divset D,j))) by A75, RFUNCT_3:def 10;
then (max+ (f | (divset D,j))) . x in rng (max+ (f | (divset D,j))) by FUNCT_1:def 5;
then A77: (max+ (f | (divset D,j))) . x in rng ((max+ f) | (divset D,j)) by RFUNCT_3:47;
A78: (max+ (f | (divset D,j))) . x = max+ ((f | (divset D,j)) . x) by A76, RFUNCT_3:def 10
.= max ((f | (divset D,j)) . x),0 by RFUNCT_3:def 1 ;

now

per cases ( r < 0 or r >= 0 ) ;

suppose r < 0 ; :: thesis: ex r being Real st
( r in rng ((max+ f) | (divset D,j)) & r < 0 + s )

then 0 in rng ((max+ f) | (divset D,j)) by A75, A77, A78, XXREAL_0:def 10;
hence ex r being Real st
( r in rng ((max+ f) | (divset D,j)) & r < 0 + s ) by A72; :: thesis: verum

end;

suppose r >= 0 ; :: thesis: ex r being Real st
( r in rng ((max+ f) | (divset D,j)) & r < 0 + s )

then ( r in rng ((max+ f) | (divset D,j)) & r < 0 + s ) by A56, A74, A75, A77, A78, XREAL_1:21, XXREAL_0:def 10;
hence ex r being Real st
( r in rng ((max+ f) | (divset D,j)) & r < 0 + s ) ; :: thesis: verum

end;

end;

end;

hence ex r being real number st
( r in rng ((max+ f) | (divset D,j)) & r < 0 + s ) ; :: thesis: verum

end;

hence ( ( for r being real number st r in rng ((max+ f) | (divset D,j)) holds
0 <= r ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in rng ((max+ f) | (divset D,j)) & r < 0 + s ) ) ) by A70; :: thesis: verum

end;

hence lower_bound (rng ((max+ f) | (divset D,j))) = 0 by A35, A36, SEQ_4:def 5; :: thesis: verum

end;

hence (upper_bound (rng (f | (divset D,j)))) - (lower_bound (rng (f | (divset D,j)))) >= (upper_bound (rng ((max+ f) | (divset D,j)))) - (lower_bound (rng ((max+ f) | (divset D,j)))) by A56, XREAL_1:15; :: thesis: verum

end;

suppose A79: ( upper_bound (rng (f | (divset D,j))) <= 0 & lower_bound (rng (f | (divset D,j))) <= 0 ) ; :: thesis: (upper_bound (rng (f | (divset D,j)))) - (lower_bound (rng (f | (divset D,j)))) >= (upper_bound (rng ((max+ f) | (divset D,j)))) - (lower_bound (rng ((max+ f) | (divset D,j))))

( upper_bound (rng ((max+ f) | (divset D,j))) = 0 & lower_bound (rng ((max+ f) | (divset D,j))) = 0 )

proof

( ( for r being real number st r in rng ((max+ f) | (divset D,j)) holds
r <= 0 ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in rng ((max+ f) | (divset D,j)) & 0 - s < r ) ) )

proof

A80: for r being real number st r in rng ((max+ f) | (divset D,j)) holds
r <= 0

proof

let r be real number ; :: thesis: ( r in rng ((max+ f) | (divset D,j)) implies r <= 0 )
assume r in rng ((max+ f) | (divset D,j)) ; :: thesis: r <= 0
then consider x being Element of A such that
A81: ( x in dom ((max+ f) | (divset D,j)) & r = ((max+ f) | (divset D,j)) . x ) by PARTFUN1:26;
A82: r = (max+ (f | (divset D,j))) . x by A81, RFUNCT_3:47;
A83: x in dom (max+ (f | (divset D,j))) by A81, RFUNCT_3:47;
then x in dom (f | (divset D,j)) by RFUNCT_3:def 10;
then (f | (divset D,j)) . x in rng (f | (divset D,j)) by FUNCT_1:def 5;
then A84: (f | (divset D,j)) . x <= upper_bound (rng (f | (divset D,j))) by A34, SEQ_4:def 4;
r = max+ ((f | (divset D,j)) . x) by A82, A83, RFUNCT_3:def 10
.= max ((f | (divset D,j)) . x),0 by RFUNCT_3:def 1
.= 0 by A79, A84, XXREAL_0:def 10 ;
hence r <= 0 ; :: thesis: verum

end;

for s being real number st 0 < s holds
ex r being real number st
( r in rng ((max+ f) | (divset D,j)) & 0 - s < r )

proof

let s be real number ; :: thesis: ( 0 < s implies ex r being real number st
( r in rng ((max+ f) | (divset D,j)) & 0 - s < r ) )
assume s > 0 ; :: thesis: ex r being real number st
( r in rng ((max+ f) | (divset D,j)) & 0 - s < r )
then 0 + s > 0 ;
then A85: 0 - s < 0 ;
consider r being Real such that
A86: r in rng ((max+ f) | (divset D,j)) by A35, SUBSET_1:10;
consider x being Element of A such that
A87: ( x in dom ((max+ f) | (divset D,j)) & r = ((max+ f) | (divset D,j)) . x ) by A86, PARTFUN1:26;
( x in dom (max+ (f | (divset D,j))) & r = (max+ (f | (divset D,j))) . x ) by A87, RFUNCT_3:47;
then r >= 0 by RFUNCT_3:40;
hence ex r being real number st
( r in rng ((max+ f) | (divset D,j)) & 0 - s < r ) by A85, A86; :: thesis: verum

end;

hence ( ( for r being real number st r in rng ((max+ f) | (divset D,j)) holds
r <= 0 ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in rng ((max+ f) | (divset D,j)) & 0 - s < r ) ) ) by A80; :: thesis: verum

end;

hence upper_bound (rng ((max+ f) | (divset D,j))) = 0 by A35, A36, SEQ_4:def 4; :: thesis: lower_bound (rng ((max+ f) | (divset D,j))) = 0
( ( for r being real number st r in rng ((max+ f) | (divset D,j)) holds
0 <= r ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in rng ((max+ f) | (divset D,j)) & r < 0 + s ) ) )

proof

A88: for r being real number st r in rng ((max+ f) | (divset D,j)) holds
0 <= r

proof

let r be real number ; :: thesis: ( r in rng ((max+ f) | (divset D,j)) implies 0 <= r )
assume r in rng ((max+ f) | (divset D,j)) ; :: thesis: 0 <= r
then consider x being Element of A such that
A89: ( x in dom ((max+ f) | (divset D,j)) & r = ((max+ f) | (divset D,j)) . x ) by PARTFUN1:26;
r = (max+ (f | (divset D,j))) . x by A89, RFUNCT_3:47;
hence 0 <= r by RFUNCT_3:40; :: thesis: verum

end;

for s being real number st 0 < s holds
ex r being real number st
( r in rng ((max+ f) | (divset D,j)) & r < 0 + s )

proof

let s be real number ; :: thesis: ( 0 < s implies ex r being real number st
( r in rng ((max+ f) | (divset D,j)) & r < 0 + s ) )
assume A90: s > 0 ; :: thesis: ex r being real number st
( r in rng ((max+ f) | (divset D,j)) & r < 0 + s )
consider r being Real such that
A91: r in rng ((max+ f) | (divset D,j)) by A35, SUBSET_1:10;
consider x being Element of A such that
A92: ( x in dom ((max+ f) | (divset D,j)) & r = ((max+ f) | (divset D,j)) . x ) by A91, PARTFUN1:26;
A93: ( x in dom (max+ (f | (divset D,j))) & r = (max+ (f | (divset D,j))) . x ) by A92, RFUNCT_3:47;
then A94: ( x in dom (f | (divset D,j)) & r = (max+ (f | (divset D,j))) . x ) by RFUNCT_3:def 10;
A95: r = max+ ((f | (divset D,j)) . x) by A93, RFUNCT_3:def 10
.= max ((f | (divset D,j)) . x),0 by RFUNCT_3:def 1 ;
(f | (divset D,j)) . x in rng (f | (divset D,j)) by A94, FUNCT_1:def 5;
then (f | (divset D,j)) . x <= upper_bound (rng (f | (divset D,j))) by A34, SEQ_4:def 4;
then r = 0 by A79, A95, XXREAL_0:def 10;
hence ex r being real number st
( r in rng ((max+ f) | (divset D,j)) & r < 0 + s ) by A90, A91; :: thesis: verum

end;

hence ( ( for r being real number st r in rng ((max+ f) | (divset D,j)) holds
0 <= r ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in rng ((max+ f) | (divset D,j)) & r < 0 + s ) ) ) by A88; :: thesis: verum

end;

hence lower_bound (rng ((max+ f) | (divset D,j))) = 0 by A35, A36, SEQ_4:def 5; :: thesis: verum

end;

hence (upper_bound (rng (f | (divset D,j)))) - (lower_bound (rng (f | (divset D,j)))) >= (upper_bound (rng ((max+ f) | (divset D,j)))) - (lower_bound (rng ((max+ f) | (divset D,j)))) by A24, XREAL_1:50; :: thesis: verum

end;

end;

end;

hence (upper_bound (rng (f | (divset D,j)))) - (lower_bound (rng (f | (divset D,j)))) >= (upper_bound (rng ((max+ f) | (divset D,j)))) - (lower_bound (rng ((max+ f) | (divset D,j)))) ; :: thesis: verum

end;

vol (divset D,j) >= 0 by INTEGRA1:11;
hence (UV1 - LV1) . j <= (UV - LV) . j by A21, A23, A27, XREAL_1:66; :: thesis: verum

end;

then A96: osc1 . m <= osc . m by A16, A18, RVSUM_1:112;
reconsider F = UV1 - LV1 as FinSequence of REAL ;
A97: osc1 . m >= 0

proof

for j being Nat st j in dom F holds
0 <= F . j

proof

let j be Nat; :: thesis: ( j in dom F implies 0 <= F . j )
assume A98: j in dom F ; :: thesis: 0 <= F . j
set r = F . j;
j in Seg (len F) by A98, FINSEQ_1:def 3;
then A99: j in Seg (len D) by FINSEQ_1:def 18;
then j in dom D by FINSEQ_1:def 3;
then ( UV1 . j = (upper_bound (rng ((max+ f) | (divset D,j)))) * (vol (divset D,j)) & LV1 . j = (lower_bound (rng ((max+ f) | (divset D,j)))) * (vol (divset D,j)) ) by INTEGRA1:def 7, INTEGRA1:def 8;
then A100: F . j = ((upper_bound (rng ((max+ f) | (divset D,j)))) * (vol (divset D,j))) - ((lower_bound (rng ((max+ f) | (divset D,j)))) * (vol (divset D,j))) by A98, VALUED_1:13
.= ((upper_bound (rng ((max+ f) | (divset D,j)))) - (lower_bound (rng ((max+ f) | (divset D,j))))) * (vol (divset D,j)) ;
A101: (upper_bound (rng ((max+ f) | (divset D,j)))) - (lower_bound (rng ((max+ f) | (divset D,j)))) >= 0

proof

( rng ((max+ f) | (divset D,j)) is bounded & ex r being Real st r in rng ((max+ f) | (divset D,j)) )

proof

consider r being Real such that
A102: r in divset D,j by SUBSET_1:10;
j in dom D by A99, FINSEQ_1:def 3;
then divset D,j c= A by INTEGRA1:10;
then r in A by A102;
then r in dom f by FUNCT_2:def 1;
then r in (dom f) /\ (divset D,j) by A102, XBOOLE_0:def 4;
then r in dom (f | (divset D,j)) by RELAT_1:90;
then r in dom (max+ (f | (divset D,j))) by RFUNCT_3:def 10;
then r in dom ((max+ f) | (divset D,j)) by RFUNCT_3:47;
then A103: ((max+ f) | (divset D,j)) . r in rng ((max+ f) | (divset D,j)) by FUNCT_1:def 5;
( f | A is bounded_above & f | A is bounded_below ) by A1;
then ( (max+ f) | A is bounded_above & (max+ f) | A is bounded_below ) by Th14, Th15;
then ( rng (max+ f) is bounded_above & rng (max+ f) is bounded_below ) by INTEGRA1:13, INTEGRA1:15;
then rng (max+ f) is bounded ;
hence rng ((max+ f) | (divset D,j)) is bounded by RELAT_1:99, XXREAL_2:45; :: thesis: ex r being Real st r in rng ((max+ f) | (divset D,j))
thus ex r being Real st r in rng ((max+ f) | (divset D,j)) by A103; :: thesis: verum

end;

hence (upper_bound (rng ((max+ f) | (divset D,j)))) - (lower_bound (rng ((max+ f) | (divset D,j)))) >= 0 by SEQ_4:24, XREAL_1:50; :: thesis: verum

end;

vol (divset D,j) >= 0 by INTEGRA1:11;
hence 0 <= F . j by A100, A101; :: thesis: verum

end;

hence osc1 . m >= 0 by A18, RVSUM_1:114; :: thesis: verum

end;

then A104: abs ((osc1 . m) - 0 ) = osc1 . m by ABSVALUE:def 1;
abs (osc . m) = osc . m by A96, A97, ABSVALUE:def 1;
hence abs ((osc1 . m) - 0 ) < a by A14, A96, A104, XXREAL_0:2; :: thesis: verum

end;

hence ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((osc1 . m) - 0 ) < a ; :: thesis: verum

end;

then osc1 is convergent by SEQ_2:def 6;
then lim ((upper_sum (max+ f),T) - (lower_sum (max+ f),T)) = 0 by A12, SEQ_2:def 7;
hence (lim (upper_sum (max+ f),T)) - (lim (lower_sum (max+ f),T)) = 0 by A7, SEQ_2:26; :: thesis: verum

end;

hence max+ f is integrable by A3, A4, Th12; :: thesis: verum