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: max+ f is total by Th13;
A4: (max+ f) | A is bounded_below by Th15;
A5: (max+ f) | A is bounded_above by A1, Th14;
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
A6: delta T is convergent and
A7: lim (delta T) = 0 ; :: thesis: (lim (upper_sum ((max+ f),T))) - (lim (lower_sum ((max+ f),T))) = 0
A8: lower_sum (f,T) is convergent by A1, A6, A7, Th8;
A9: upper_sum (f,T) is convergent by A1, A6, A7, Th9;
then A10: (upper_sum (f,T)) - (lower_sum (f,T)) is convergent by A8;
reconsider osc1 = (upper_sum ((max+ f),T)) - (lower_sum ((max+ f),T)) as Real_Sequence ;
reconsider osc = (upper_sum (f,T)) - (lower_sum (f,T)) as Real_Sequence ;
(lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = 0 by A1, A2, A6, A7, Th12;
then A11: lim ((upper_sum (f,T)) - (lower_sum (f,T))) = 0 by A9, A8, SEQ_2:12;
A12: for a being Real st 0 < a holds
ex n being Nat st
for m being Nat st n <= m holds
|.((osc1 . m) - 0).| < a

proof

let a be Real; :: thesis: ( 0 < a implies ex n being Nat st
for m being Nat st n <= m holds
|.((osc1 . m) - 0).| < a )
assume 0 < a ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((osc1 . m) - 0).| < a
then consider n being Nat such that
A13: for m being Nat st n <= m holds
|.((osc . m) - 0).| < a by A10, A11, SEQ_2:def 7;
take n ; :: thesis: for m being Nat st n <= m holds
|.((osc1 . m) - 0).| < a
let m be Nat; :: thesis: ( n <= m implies |.((osc1 . m) - 0).| < a )
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
reconsider D = T . mm as Division of A ;
len (upper_volume (f,D)) = len D by INTEGRA1:def 6;
then reconsider UV = upper_volume (f,D) as Element of (len D) -tuples_on REAL by FINSEQ_2:133;
len (lower_volume (f,D)) = len D by INTEGRA1:def 7;
then reconsider LV = lower_volume (f,D) as Element of (len D) -tuples_on REAL by FINSEQ_2:133;
len (upper_volume ((max+ f),D)) = len D by INTEGRA1:def 6;
then reconsider UV1 = upper_volume ((max+ f),D) as Element of (len D) -tuples_on REAL by FINSEQ_2:133;
len (lower_volume ((max+ f),D)) = len D by INTEGRA1:def 7;
then reconsider LV1 = lower_volume ((max+ f),D) as Element of (len D) -tuples_on REAL by FINSEQ_2:133;
reconsider F = UV1 - LV1 as FinSequence of REAL ;
osc1 . m = ((upper_sum ((max+ f),T)) . m) + ((- (lower_sum ((max+ f),T))) . m) by SEQ_1:7
.= ((upper_sum ((max+ f),T)) . m) + (- ((lower_sum ((max+ f),T)) . m)) by SEQ_1:10
.= ((upper_sum ((max+ f),T)) . m) - ((lower_sum ((max+ f),T)) . m)
.= (upper_sum ((max+ f),(T . mm))) - ((lower_sum ((max+ f),T)) . m) by INTEGRA2:def 2
.= (upper_sum ((max+ f),(T . mm))) - (lower_sum ((max+ f),(T . mm))) by INTEGRA2:def 3
.= (Sum (upper_volume ((max+ f),D))) - (lower_sum ((max+ f),(T . mm))) by INTEGRA1:def 8
.= (Sum (upper_volume ((max+ f),D))) - (Sum (lower_volume ((max+ f),D))) by INTEGRA1:def 9 ;
then A14: osc1 . m = Sum (UV1 - LV1) by RVSUM_1:90;
A15: 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 )
set x = (UV1 - LV1) . j;
set y = (UV - LV) . j;
assume A16: j in Seg (len D) ; :: thesis: (UV1 - LV1) . j <= (UV - LV) . j
then A17: j in dom D by FINSEQ_1:def 3;
then A18: LV1 . j = (lower_bound (rng ((max+ f) | (divset (D,j))))) * (vol (divset (D,j))) by INTEGRA1:def 7;
A19: ( rng (f | (divset (D,j))) is real-bounded & ex r being Real st r in rng (f | (divset (D,j))) )

proof

A20: rng f is bounded_below by A1, INTEGRA1:11;
rng f is bounded_above by A1, INTEGRA1:13;
hence rng (f | (divset (D,j))) is real-bounded by A20, RELAT_1:70, XXREAL_2:45; :: thesis: ex r being Real st r in rng (f | (divset (D,j)))
consider r being Element of REAL such that
A21: r in divset (D,j) by SUBSET_1:4;
j in dom D by A16, FINSEQ_1:def 3;
then divset (D,j) c= A by INTEGRA1:8;
then r in A by A21;
then r in dom f by FUNCT_2:def 1;
then f . r in rng (f | (divset (D,j))) by A21, FUNCT_1:50;
hence ex r being Real st r in rng (f | (divset (D,j))) ; :: thesis: verum

end;

A22: (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 m1 = lower_bound (rng ((max+ f) | (divset (D,j))));
set M1 = upper_bound (rng ((max+ f) | (divset (D,j))));
set m = lower_bound (rng (f | (divset (D,j))));
set M = upper_bound (rng (f | (divset (D,j))));
A23: dom f = dom (max+ f) by RFUNCT_3:def 10;
A24: j in dom D by A16, FINSEQ_1:def 3;
A25: rng (f | (divset (D,j))) is bounded_above by A1, Th18;
dom (f | (divset (D,j))) = (dom f) /\ (divset (D,j)) by RELAT_1:61;
then dom (f | (divset (D,j))) = A /\ (divset (D,j)) by FUNCT_2:def 1;
then dom (f | (divset (D,j))) <> {} by A24, INTEGRA1:8, XBOOLE_1:28;
then A26: rng (f | (divset (D,j))) <> {} by RELAT_1:42;
dom f = A by FUNCT_2:def 1;
then dom ((max+ f) | (divset (D,j))) = A /\ (divset (D,j)) by A23, RELAT_1:61;
then dom ((max+ f) | (divset (D,j))) <> {} by A24, INTEGRA1:8, XBOOLE_1:28;
then A27: rng ((max+ f) | (divset (D,j))) <> {} by RELAT_1:42;
(max+ f) | A is bounded_below by Th15;
then A28: rng ((max+ f) | (divset (D,j))) is bounded_below by Th19;
A29: rng (f | (divset (D,j))) is bounded_below by A1, Th19;
(max+ f) | A is bounded_above by A1, Th14;
then A30: rng ((max+ f) | (divset (D,j))) is bounded_above by Th18;

now :: 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)))))

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 A19, SEQ_4:11;

suppose A31: ( 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)))))

A32: 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
A33: x in dom ((max+ f) | (divset (D,j))) and
A34: r = ((max+ f) | (divset (D,j))) . x by PARTFUN1:3;
A35: r = (max+ (f | (divset (D,j)))) . x by A34, RFUNCT_3:44;
A36: x in dom (max+ (f | (divset (D,j)))) by A33, RFUNCT_3:44;
then A37: x in dom (f | (divset (D,j))) by RFUNCT_3:def 10;

now :: thesis: r <= upper_bound (rng (f | (divset (D,j))))

per cases ( r = 0 or r > 0 ) by A35, RFUNCT_3:37;

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

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

end;

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

r = max+ ((f | (divset (D,j))) . x) by A35, A36, 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 A38, XXREAL_0:def 10;
then r in rng (f | (divset (D,j))) by A37, FUNCT_1:def 3;
hence r <= upper_bound (rng (f | (divset (D,j)))) by A25, SEQ_4:def 1; :: thesis: verum

end;

end;

end;

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

end;

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

proof

let s be Real; :: thesis: ( 0 < s implies ex r being Real 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 st
( r in rng ((max+ f) | (divset (D,j))) & r < (lower_bound (rng (f | (divset (D,j))))) + s )
then consider r being Real such that
A40: r in rng (f | (divset (D,j))) and
A41: r < (lower_bound (rng (f | (divset (D,j))))) + s by A26, A29, SEQ_4:def 2;
reconsider r = r as Real ;
r in rng ((max+ f) | (divset (D,j)))

proof

A42: r >= lower_bound (rng (f | (divset (D,j)))) by A29, A40, SEQ_4:def 2;
consider x being Element of A such that
A43: x in dom (f | (divset (D,j))) and
A44: r = (f | (divset (D,j))) . x by A40, PARTFUN1:3;
A45: x in dom (max+ (f | (divset (D,j)))) by A43, RFUNCT_3:def 10;
then (max+ (f | (divset (D,j)))) . x = max+ r by A44, RFUNCT_3:def 10
.= max (r,0) by RFUNCT_3:def 1
.= r by A31, A42, XXREAL_0:def 10 ;
then r in rng (max+ (f | (divset (D,j)))) by A45, FUNCT_1:def 3;
hence r in rng ((max+ f) | (divset (D,j))) by RFUNCT_3:44; :: thesis: verum

end;

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

end;

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

proof

let r be Real; :: 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
A47: x in dom ((max+ f) | (divset (D,j))) and
A48: r = ((max+ f) | (divset (D,j))) . x by PARTFUN1:3;
A49: x in dom (max+ (f | (divset (D,j)))) by A47, RFUNCT_3:44;
x in dom (max+ (f | (divset (D,j)))) by A47, RFUNCT_3:44;
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 3;
then A50: (f | (divset (D,j))) . x >= lower_bound (rng (f | (divset (D,j)))) by A29, SEQ_4:def 2;
r = (max+ (f | (divset (D,j)))) . x by A48, RFUNCT_3:44
.= max+ ((f | (divset (D,j))) . x) by A49, RFUNCT_3:def 10
.= max (((f | (divset (D,j))) . x),0) by RFUNCT_3:def 1 ;
hence lower_bound (rng (f | (divset (D,j)))) <= r by A31, A50, XXREAL_0:def 10; :: thesis: verum

end;

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

proof

let s be Real; :: thesis: ( 0 < s implies ex r being Real 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 st
( r in rng ((max+ f) | (divset (D,j))) & (upper_bound (rng (f | (divset (D,j))))) - s < r )
then consider r being Real such that
A51: r in rng (f | (divset (D,j))) and
A52: (upper_bound (rng (f | (divset (D,j))))) - s < r by A26, A25, SEQ_4:def 1;
r in rng ((max+ f) | (divset (D,j)))

proof

reconsider r1 = r as Real ;
consider x being Element of A such that
A53: x in dom (f | (divset (D,j))) and
A54: r = (f | (divset (D,j))) . x by A51, PARTFUN1:3;
A55: r >= lower_bound (rng (f | (divset (D,j)))) by A29, A51, SEQ_4:def 2;
A56: x in dom (max+ (f | (divset (D,j)))) by A53, RFUNCT_3:def 10;
then (max+ (f | (divset (D,j)))) . x = max+ r1 by A54, RFUNCT_3:def 10
.= max (r,0) by RFUNCT_3:def 1
.= r by A31, A55, XXREAL_0:def 10 ;
then r in rng (max+ (f | (divset (D,j)))) by A56, FUNCT_1:def 3;
hence r in rng ((max+ f) | (divset (D,j))) by RFUNCT_3:44; :: thesis: verum

end;

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

end;

then upper_bound (rng ((max+ f) | (divset (D,j)))) = upper_bound (rng (f | (divset (D,j)))) by A27, A30, A32, SEQ_4:def 1;
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 A27, A28, A46, A39, SEQ_4:def 2; :: thesis: verum

end;

suppose A57: ( 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)))))

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

proof

let s be Real; :: thesis: ( 0 < s implies ex r being Real st
( r in rng ((max+ f) | (divset (D,j))) & r < 0 + s ) )
assume A59: s > 0 ; :: thesis: ex r being Real st
( r in rng ((max+ f) | (divset (D,j))) & r < 0 + s )
then consider r being Real such that
A60: r in rng (f | (divset (D,j))) and
A61: r < (lower_bound (rng (f | (divset (D,j))))) + s by A26, A29, SEQ_4:def 2;
consider x being Element of A such that
A62: x in dom (f | (divset (D,j))) and
A63: r = (f | (divset (D,j))) . x by A60, PARTFUN1:3;
A64: x in dom (max+ (f | (divset (D,j)))) by A62, RFUNCT_3:def 10;
then A65: (max+ (f | (divset (D,j)))) . x = max+ ((f | (divset (D,j))) . x) by RFUNCT_3:def 10
.= max (((f | (divset (D,j))) . x),0) by RFUNCT_3:def 1 ;
(max+ (f | (divset (D,j)))) . x in rng (max+ (f | (divset (D,j)))) by A64, FUNCT_1:def 3;
then A66: (max+ (f | (divset (D,j)))) . x in rng ((max+ f) | (divset (D,j))) by RFUNCT_3:44;
A67: r - s < lower_bound (rng (f | (divset (D,j)))) by A61, XREAL_1:19;

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

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 A63, A66, A65, XXREAL_0:def 10;
hence ex r being Real st
( r in rng ((max+ f) | (divset (D,j))) & r < 0 + s ) by A59; :: thesis: verum

end;

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

A69: r < 0 + s by A57, A67, XREAL_1:19;
r in rng ((max+ f) | (divset (D,j))) by A63, A66, A65, A68, XXREAL_0:def 10;
hence ex r being Real st
( r in rng ((max+ f) | (divset (D,j))) & r < 0 + s ) by A69; :: thesis: verum

end;

end;

end;

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

end;

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

proof

let r be Real; :: 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:44;
then ex x being Element of A st
( x in dom (max+ (f | (divset (D,j)))) & r = (max+ (f | (divset (D,j)))) . x ) by PARTFUN1:3;
hence 0 <= r by RFUNCT_3:37; :: thesis: verum

end;

then A70: lower_bound (rng ((max+ f) | (divset (D,j)))) = 0 by A27, A28, A58, SEQ_4:def 2;
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
A71: x in dom ((max+ f) | (divset (D,j))) and
A72: r = ((max+ f) | (divset (D,j))) . x by PARTFUN1:3;
A73: r = (max+ (f | (divset (D,j)))) . x by A72, RFUNCT_3:44;
A74: x in dom (max+ (f | (divset (D,j)))) by A71, RFUNCT_3:44;
then A75: x in dom (f | (divset (D,j))) by RFUNCT_3:def 10;

now :: thesis: r <= upper_bound (rng (f | (divset (D,j))))

per cases ( r = 0 or r > 0 ) by A73, RFUNCT_3:37;

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

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

end;

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

r = max+ ((f | (divset (D,j))) . x) by A73, A74, 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 A76, XXREAL_0:def 10;
then r in rng (f | (divset (D,j))) by A75, FUNCT_1:def 3;
hence r <= upper_bound (rng (f | (divset (D,j)))) by A25, SEQ_4:def 1; :: thesis: verum

end;

end;

end;

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

end;

then A77: for r being Real st r in rng ((max+ f) | (divset (D,j))) holds
r <= upper_bound (rng (f | (divset (D,j)))) ;
for s being Real st 0 < s holds
ex r being Real st
( r in rng ((max+ f) | (divset (D,j))) & (upper_bound (rng (f | (divset (D,j))))) - s < r )

proof

assume ex s being Real st
( 0 < s & ( for r being Real 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 such that
A78: s > 0 and
A79: for r being Real st r in rng ((max+ f) | (divset (D,j))) holds
(upper_bound (rng (f | (divset (D,j))))) - s >= r ;
consider r1 being Real such that
A80: r1 in rng (f | (divset (D,j))) and
A81: (upper_bound (rng (f | (divset (D,j))))) - s < r1 by A26, A25, A78, SEQ_4:def 1;
consider x being Element of A such that
A82: x in dom (f | (divset (D,j))) and
A83: r1 = (f | (divset (D,j))) . x by A80, PARTFUN1:3;
A84: x in dom (max+ (f | (divset (D,j)))) by A82, RFUNCT_3:def 10;
then x in dom ((max+ f) | (divset (D,j))) by RFUNCT_3:44;
then A85: ((max+ f) | (divset (D,j))) . x in rng ((max+ f) | (divset (D,j))) by FUNCT_1:def 3;
(max+ (f | (divset (D,j)))) . x >= 0 by RFUNCT_3:37;
then ((max+ f) | (divset (D,j))) . x >= 0 by RFUNCT_3:44;
then A86: (upper_bound (rng (f | (divset (D,j))))) - s >= 0 by A79, A85;
((max+ f) | (divset (D,j))) . x = (max+ (f | (divset (D,j)))) . x by RFUNCT_3:44
.= max+ ((f | (divset (D,j))) . x) by A84, RFUNCT_3:def 10
.= max (r1,0) by A83, RFUNCT_3:def 1
.= r1 by A81, A86, XXREAL_0:def 10 ;
hence contradiction by A79, A81, A85; :: thesis: verum

end;

then upper_bound (rng ((max+ f) | (divset (D,j)))) = upper_bound (rng (f | (divset (D,j)))) by A27, A30, A77, SEQ_4:def 1;
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 A57, A70, XREAL_1:13; :: thesis: verum

end;

suppose A87: ( 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)))))

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

proof

let s be Real; :: thesis: ( 0 < s implies ex r being Real st
( r in rng ((max+ f) | (divset (D,j))) & r < 0 + s ) )
assume A89: s > 0 ; :: thesis: ex r being Real st
( r in rng ((max+ f) | (divset (D,j))) & r < 0 + s )
consider r being Element of REAL such that
A90: r in rng ((max+ f) | (divset (D,j))) by A27, SUBSET_1:4;
consider x being Element of A such that
A91: x in dom ((max+ f) | (divset (D,j))) and
A92: r = ((max+ f) | (divset (D,j))) . x by A90, PARTFUN1:3;
A93: x in dom (max+ (f | (divset (D,j)))) by A91, RFUNCT_3:44;
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 3;
then A94: (f | (divset (D,j))) . x <= upper_bound (rng (f | (divset (D,j)))) by A25, SEQ_4:def 1;
r = (max+ (f | (divset (D,j)))) . x by A92, RFUNCT_3:44;
then 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 ;
then r = 0 by A87, A94, XXREAL_0:def 10;
hence ex r being Real st
( r in rng ((max+ f) | (divset (D,j))) & r < 0 + s ) by A89, A90; :: thesis: verum

end;

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

proof

let r be Real; :: 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
x in dom ((max+ f) | (divset (D,j))) and
A95: r = ((max+ f) | (divset (D,j))) . x by PARTFUN1:3;
r = (max+ (f | (divset (D,j)))) . x by A95, RFUNCT_3:44;
hence 0 <= r by RFUNCT_3:37; :: thesis: verum

end;

then A96: lower_bound (rng ((max+ f) | (divset (D,j)))) = 0 by A27, A28, A88, SEQ_4:def 2;
A97: for r being Real st r in rng ((max+ f) | (divset (D,j))) holds
r <= 0

proof

let r be Real; :: 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
A98: x in dom ((max+ f) | (divset (D,j))) and
A99: r = ((max+ f) | (divset (D,j))) . x by PARTFUN1:3;
A100: x in dom (max+ (f | (divset (D,j)))) by A98, RFUNCT_3:44;
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 3;
then A101: (f | (divset (D,j))) . x <= upper_bound (rng (f | (divset (D,j)))) by A25, SEQ_4:def 1;
r = (max+ (f | (divset (D,j)))) . x by A99, RFUNCT_3:44;
then r = max+ ((f | (divset (D,j))) . x) by A100, RFUNCT_3:def 10
.= max (((f | (divset (D,j))) . x),0) by RFUNCT_3:def 1
.= 0 by A87, A101, XXREAL_0:def 10 ;
hence r <= 0 ; :: thesis: verum

end;

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

proof

let s be Real; :: thesis: ( 0 < s implies ex r being Real st
( r in rng ((max+ f) | (divset (D,j))) & 0 - s < r ) )
assume A102: s > 0 ; :: thesis: ex r being Real st
( r in rng ((max+ f) | (divset (D,j))) & 0 - s < r )
consider r being Element of REAL such that
A103: r in rng ((max+ f) | (divset (D,j))) by A27, SUBSET_1:4;
consider x being Element of A such that
x in dom ((max+ f) | (divset (D,j))) and
A104: r = ((max+ f) | (divset (D,j))) . x by A103, PARTFUN1:3;
r = (max+ (f | (divset (D,j)))) . x by A104, RFUNCT_3:44;
then r >= 0 by RFUNCT_3:37;
hence ex r being Real st
( r in rng ((max+ f) | (divset (D,j))) & 0 - s < r ) by A102, A103; :: thesis: verum

end;

then upper_bound (rng ((max+ f) | (divset (D,j)))) = 0 by A27, A30, A97, SEQ_4:def 1;
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 A19, A96, SEQ_4:11, XREAL_1:48; :: 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;

A105: LV . j = (lower_bound (rng (f | (divset (D,j))))) * (vol (divset (D,j))) by A17, INTEGRA1:def 7;
UV . j = (upper_bound (rng (f | (divset (D,j))))) * (vol (divset (D,j))) by A17, INTEGRA1:def 6;
then A106: (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 A105, RVSUM_1:27
.= ((upper_bound (rng (f | (divset (D,j))))) - (lower_bound (rng (f | (divset (D,j)))))) * (vol (divset (D,j))) ;
UV1 . j = (upper_bound (rng ((max+ f) | (divset (D,j))))) * (vol (divset (D,j))) by A17, INTEGRA1:def 6;
then A107: (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 A18, RVSUM_1:27
.= ((upper_bound (rng ((max+ f) | (divset (D,j))))) - (lower_bound (rng ((max+ f) | (divset (D,j)))))) * (vol (divset (D,j))) ;
vol (divset (D,j)) >= 0 by INTEGRA1:9;
hence (UV1 - LV1) . j <= (UV - LV) . j by A107, A106, A22, XREAL_1:64; :: thesis: verum

end;

assume n <= m ; :: thesis: |.((osc1 . m) - 0).| < a
then A108: |.((osc . m) - 0).| < a by A13;
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 )
set r = F . j;
(max+ f) | A is bounded_below by Th15;
then A109: rng (max+ f) is bounded_below by INTEGRA1:11;
assume A110: j in dom F ; :: thesis: 0 <= F . j
j in Seg (len F) by A110, FINSEQ_1:def 3;
then A111: j in Seg (len D) by CARD_1:def 7;
then A112: j in dom D by FINSEQ_1:def 3;
then A113: LV1 . j = (lower_bound (rng ((max+ f) | (divset (D,j))))) * (vol (divset (D,j))) by INTEGRA1:def 7;
A114: ex r being Real st r in rng ((max+ f) | (divset (D,j)))

proof

consider r being Element of REAL such that
A115: r in divset (D,j) by SUBSET_1:4;
j in dom D by A111, FINSEQ_1:def 3;
then divset (D,j) c= A by INTEGRA1:8;
then r in A by A115;
then r in dom f by FUNCT_2:def 1;
then r in (dom f) /\ (divset (D,j)) by A115, XBOOLE_0:def 4;
then r in dom (f | (divset (D,j))) by RELAT_1:61;
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:44;
then ((max+ f) | (divset (D,j))) . r in rng ((max+ f) | (divset (D,j))) by FUNCT_1:def 3;
hence ex r being Real st r in rng ((max+ f) | (divset (D,j))) ; :: thesis: verum

end;

(max+ f) | A is bounded_above by A1, Th14;
then rng (max+ f) is bounded_above by INTEGRA1:13;
then rng ((max+ f) | (divset (D,j))) is real-bounded by A109, RELAT_1:70, XXREAL_2:45;
then A116: (upper_bound (rng ((max+ f) | (divset (D,j))))) - (lower_bound (rng ((max+ f) | (divset (D,j))))) >= 0 by A114, SEQ_4:11, XREAL_1:48;
UV1 . j = (upper_bound (rng ((max+ f) | (divset (D,j))))) * (vol (divset (D,j))) by A112, INTEGRA1:def 6;
then A117: 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 A110, A113, VALUED_1:13
.= ((upper_bound (rng ((max+ f) | (divset (D,j))))) - (lower_bound (rng ((max+ f) | (divset (D,j)))))) * (vol (divset (D,j))) ;
vol (divset (D,j)) >= 0 by INTEGRA1:9;
hence 0 <= F . j by A117, A116; :: thesis: verum

end;

then A118: osc1 . m >= 0 by A14, RVSUM_1:84;
then A119: |.((osc1 . m) - 0).| = osc1 . m by ABSVALUE:def 1;
osc . m = ((upper_sum (f,T)) . m) + ((- (lower_sum (f,T))) . m) by SEQ_1:7
.= ((upper_sum (f,T)) . m) + (- ((lower_sum (f,T)) . m)) by SEQ_1:10
.= ((upper_sum (f,T)) . m) - ((lower_sum (f,T)) . m)
.= (upper_sum (f,(T . mm))) - ((lower_sum (f,T)) . m) by INTEGRA2:def 2
.= (upper_sum (f,(T . mm))) - (lower_sum (f,(T . mm))) by INTEGRA2:def 3
.= (Sum (upper_volume (f,D))) - (lower_sum (f,(T . mm))) by INTEGRA1:def 8
.= (Sum (upper_volume (f,D))) - (Sum (lower_volume (f,D))) by INTEGRA1:def 9 ;
then osc . m = Sum (UV - LV) by RVSUM_1:90;
then A120: osc1 . m <= osc . m by A14, A15, RVSUM_1:82;
then |.(osc . m).| = osc . m by A118, ABSVALUE:def 1;
hence |.((osc1 . m) - 0).| < a by A108, A120, A119, XXREAL_0:2; :: thesis: verum

end;

then osc1 is convergent by SEQ_2:def 6;
then A121: lim ((upper_sum ((max+ f),T)) - (lower_sum ((max+ f),T))) = 0 by A12, SEQ_2:def 7;
A122: lower_sum ((max+ f),T) is convergent by A3, A5, A4, A6, A7, Th8;
upper_sum ((max+ f),T) is convergent by A3, A5, A4, A6, A7, Th9;
hence (lim (upper_sum ((max+ f),T))) - (lim (lower_sum ((max+ f),T))) = 0 by A122, A121, SEQ_2:12; :: thesis: verum

end;

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