let a be Real; :: thesis: for A being closed-interval Subset of REAL
for f, g, h being Function of A,REAL st f | A is bounded & f is integrable & g | A is bounded & g is integrable & h | A is bounded & a > 0 & ( for x, y being Real st x in A & y in A holds
abs ((h . x) - (h . y)) <= a * ((abs ((f . x) - (f . y))) + (abs ((g . x) - (g . y)))) ) holds
h is integrable
let A be closed-interval Subset of REAL ; :: thesis: for f, g, h being Function of A,REAL st f | A is bounded & f is integrable & g | A is bounded & g is integrable & h | A is bounded & a > 0 & ( for x, y being Real st x in A & y in A holds
abs ((h . x) - (h . y)) <= a * ((abs ((f . x) - (f . y))) + (abs ((g . x) - (g . y)))) ) holds
h is integrable
let f, g, h be Function of A,REAL ; :: thesis: ( f | A is bounded & f is integrable & g | A is bounded & g is integrable & h | A is bounded & a > 0 & ( for x, y being Real st x in A & y in A holds
abs ((h . x) - (h . y)) <= a * ((abs ((f . x) - (f . y))) + (abs ((g . x) - (g . y)))) ) implies h is integrable )
assume that
A1: f | A is bounded and
A2: f is integrable and
A3: g | A is bounded and
A4: g is integrable and
A5: h | A is bounded and
A6: a > 0 and
A7: for x, y being Real st x in A & y in A holds
abs ((h . x) - (h . y)) <= a * ((abs ((f . x) - (f . y))) + (abs ((g . x) - (g . y)))) ; :: thesis: h is integrable
for T being DivSequence of A st delta T is convergent & lim (delta T) = 0 holds
(lim (upper_sum h,T)) - (lim (lower_sum h,T)) = 0

proof

let T be DivSequence of A; :: thesis: ( delta T is convergent & lim (delta T) = 0 implies (lim (upper_sum h,T)) - (lim (lower_sum h,T)) = 0 )
assume that
A8: delta T is convergent and
A9: lim (delta T) = 0 ; :: thesis: (lim (upper_sum h,T)) - (lim (lower_sum h,T)) = 0
A10: lower_sum g,T is convergent by A3, A8, A9, Th8;
A11: upper_sum g,T is convergent by A3, A8, A9, Th9;
then A12: (upper_sum g,T) - (lower_sum g,T) is convergent by A10, SEQ_2:25;
(lim (upper_sum g,T)) - (lim (lower_sum g,T)) = 0 by A3, A4, A8, A9, Th12;
then A13: lim ((upper_sum g,T) - (lower_sum g,T)) = 0 by A11, A10, SEQ_2:26;
A14: lower_sum f,T is convergent by A1, A8, A9, Th8;
reconsider osc2 = (upper_sum h,T) - (lower_sum h,T) as Real_Sequence ;
reconsider osc1 = (upper_sum g,T) - (lower_sum g,T) as Real_Sequence ;
reconsider osc = (upper_sum f,T) - (lower_sum f,T) as Real_Sequence ;
A15: upper_sum f,T is convergent by A1, A8, A9, Th9;
(lim (upper_sum f,T)) - (lim (lower_sum f,T)) = 0 by A1, A2, A8, A9, Th12;
then A16: lim ((upper_sum f,T) - (lower_sum f,T)) = 0 by A15, A14, SEQ_2:26;
A17: (upper_sum f,T) - (lower_sum f,T) is convergent by A15, A14, SEQ_2:25;
A18: for b being real number st 0 < b holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((osc2 . m) - 0 ) < b

proof

let b be real number ; :: thesis: ( 0 < b implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((osc2 . m) - 0 ) < b )
assume b > 0 ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((osc2 . m) - 0 ) < b
then b / a > 0 by A6, XREAL_1:141;
then A19: (b / a) / 2 > 0 by XREAL_1:141;
then consider n1 being Element of NAT such that
A20: for m being Element of NAT st n1 <= m holds
abs ((osc . m) - 0 ) < (b / a) / 2 by A17, A16, SEQ_2:def 7;
consider n2 being Element of NAT such that
A21: for m being Element of NAT st n2 <= m holds
abs ((osc1 . m) - 0 ) < (b / a) / 2 by A12, A13, A19, SEQ_2:def 7;
ex n being Element of NAT st
( n1 <= n & n2 <= n )

proof

take n = max n1,n2; :: thesis: ( n is Element of REAL & n is Element of NAT & n1 <= n & n2 <= n )
reconsider n = n as Element of NAT by XXREAL_0:16;
n1 <= n by XXREAL_0:25;
hence ( n is Element of REAL & n is Element of NAT & n1 <= n & n2 <= n ) by XXREAL_0:25; :: thesis: verum

end;

then consider n being Element of NAT such that
A22: n1 <= n and
A23: n2 <= n ;
for m being Element of NAT st n <= m holds
abs ((osc2 . m) - 0 ) < b

proof

let m be Element of NAT ; :: thesis: ( n <= m implies abs ((osc2 . m) - 0 ) < b )
reconsider D = T . m as Division of A ;
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 FINSEQ_2:153;
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 FINSEQ_2:153;
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 ;
then A24: osc . m = Sum (UV - LV) by RVSUM_1:120;
len (lower_volume h,D) = len D by INTEGRA1:def 8;
then reconsider LV2 = lower_volume h,D as Element of (len D) -tuples_on REAL by FINSEQ_2:153;
len (upper_volume h,D) = len D by INTEGRA1:def 7;
then reconsider UV2 = upper_volume h,D as Element of (len D) -tuples_on REAL by FINSEQ_2:153;
len (lower_volume g,D) = len D by INTEGRA1:def 8;
then reconsider LV1 = lower_volume g,D as Element of (len D) -tuples_on REAL by FINSEQ_2:153;
len (upper_volume g,D) = len D by INTEGRA1:def 7;
then reconsider UV1 = upper_volume g,D as Element of (len D) -tuples_on REAL by FINSEQ_2:153;
reconsider H = UV - LV as FinSequence of REAL ;
reconsider G = UV1 - LV1 as FinSequence of REAL ;
reconsider F = UV2 - LV2 as FinSequence of REAL ;
osc1 . m = ((upper_sum g,T) . m) + ((- (lower_sum g,T)) . m) by SEQ_1:11
.= ((upper_sum g,T) . m) + (- ((lower_sum g,T) . m)) by SEQ_1:14
.= ((upper_sum g,T) . m) - ((lower_sum g,T) . m)
.= (upper_sum g,(T . m)) - ((lower_sum g,T) . m) by INTEGRA2:def 4
.= (upper_sum g,(T . m)) - (lower_sum g,(T . m)) by INTEGRA2:def 5
.= (Sum (upper_volume g,D)) - (lower_sum g,(T . m)) by INTEGRA1:def 9
.= (Sum (upper_volume g,D)) - (Sum (lower_volume g,D)) by INTEGRA1:def 10 ;
then A25: osc1 . m = Sum (UV1 - LV1) by RVSUM_1:120;
for j being Nat st j in dom G holds
0 <= G . j

proof

let j be Nat; :: thesis: ( j in dom G implies 0 <= G . j )
set r = G . j;
A26: rng g is bounded_below by A3, INTEGRA1:13;
assume A27: j in dom G ; :: thesis: 0 <= G . j
j in Seg (len G) by A27, FINSEQ_1:def 3;
then A28: j in Seg (len D) by FINSEQ_1:def 18;
then A29: j in dom D by FINSEQ_1:def 3;
then A30: LV1 . j = (lower_bound (rng (g | (divset D,j)))) * (vol (divset D,j)) by INTEGRA1:def 8;
A31: ex r being Real st r in rng (g | (divset D,j))

proof

consider r being Real such that
A32: r in divset D,j by SUBSET_1:10;
j in dom D by A28, FINSEQ_1:def 3;
then divset D,j c= A by INTEGRA1:10;
then r in A by A32;
then r in dom g by FUNCT_2:def 1;
then r in (dom g) /\ (divset D,j) by A32, XBOOLE_0:def 4;
then r in dom (g | (divset D,j)) by RELAT_1:90;
then (g | (divset D,j)) . r in rng (g | (divset D,j)) by FUNCT_1:def 5;
hence ex r being Real st r in rng (g | (divset D,j)) ; :: thesis: verum

end;

rng g is bounded_above by A3, INTEGRA1:15;
then rng (g | (divset D,j)) is bounded by A26, RELAT_1:99, XXREAL_2:45;
then A33: (upper_bound (rng (g | (divset D,j)))) - (lower_bound (rng (g | (divset D,j)))) >= 0 by A31, SEQ_4:24, XREAL_1:50;
UV1 . j = (upper_bound (rng (g | (divset D,j)))) * (vol (divset D,j)) by A29, INTEGRA1:def 7;
then A34: G . j = ((upper_bound (rng (g | (divset D,j)))) * (vol (divset D,j))) - ((lower_bound (rng (g | (divset D,j)))) * (vol (divset D,j))) by A27, A30, VALUED_1:13
.= ((upper_bound (rng (g | (divset D,j)))) - (lower_bound (rng (g | (divset D,j))))) * (vol (divset D,j)) ;
vol (divset D,j) >= 0 by INTEGRA1:11;
hence 0 <= G . j by A34, A33; :: thesis: verum

end;

then A35: osc1 . m >= 0 by A25, RVSUM_1:114;
assume A36: n <= m ; :: thesis: abs ((osc2 . m) - 0 ) < b
then n1 <= m by A22, XXREAL_0:2;
then A37: abs ((osc . m) - 0 ) < (b / a) / 2 by A20;
n2 <= m by A23, A36, XXREAL_0:2;
then A38: abs ((osc1 . m) - 0 ) < (b / a) / 2 by A21;
for j being Nat st j in dom H holds
0 <= H . j

proof

let j be Nat; :: thesis: ( j in dom H implies 0 <= H . j )
set r = H . j;
A39: rng f is bounded_below by A1, INTEGRA1:13;
assume A40: j in dom H ; :: thesis: 0 <= H . j
j in Seg (len H) by A40, FINSEQ_1:def 3;
then A41: j in Seg (len D) by FINSEQ_1:def 18;
then A42: j in dom D by FINSEQ_1:def 3;
then A43: LV . j = (lower_bound (rng (f | (divset D,j)))) * (vol (divset D,j)) by INTEGRA1:def 8;
A44: ex r being Real st r in rng (f | (divset D,j))

proof

consider r being Real such that
A45: r in divset D,j by SUBSET_1:10;
j in dom D by A41, FINSEQ_1:def 3;
then divset D,j c= A by INTEGRA1:10;
then r in A by A45;
then r in dom f by FUNCT_2:def 1;
then r in (dom f) /\ (divset D,j) by A45, XBOOLE_0:def 4;
then r in dom (f | (divset D,j)) by RELAT_1:90;
then (f | (divset D,j)) . r in rng (f | (divset D,j)) by FUNCT_1:def 5;
hence ex r being Real st r in rng (f | (divset D,j)) ; :: thesis: verum

end;

rng f is bounded_above by A1, INTEGRA1:15;
then rng (f | (divset D,j)) is bounded by A39, RELAT_1:99, XXREAL_2:45;
then A46: (upper_bound (rng (f | (divset D,j)))) - (lower_bound (rng (f | (divset D,j)))) >= 0 by A44, SEQ_4:24, XREAL_1:50;
UV . j = (upper_bound (rng (f | (divset D,j)))) * (vol (divset D,j)) by A42, INTEGRA1:def 7;
then A47: H . j = ((upper_bound (rng (f | (divset D,j)))) * (vol (divset D,j))) - ((lower_bound (rng (f | (divset D,j)))) * (vol (divset D,j))) by A40, A43, VALUED_1:13
.= ((upper_bound (rng (f | (divset D,j)))) - (lower_bound (rng (f | (divset D,j))))) * (vol (divset D,j)) ;
vol (divset D,j) >= 0 by INTEGRA1:11;
hence 0 <= H . j by A47, A46; :: thesis: verum

end;

then A48: osc . m >= 0 by A24, RVSUM_1:114;
then (osc . m) * (osc1 . m) >= 0 by A35;
then (abs (osc . m)) + (abs (osc1 . m)) = abs ((osc . m) + (osc1 . m)) by ABSVALUE:24;
then (abs ((osc . m) - 0 )) + (abs (osc1 . m)) = (osc . m) + (osc1 . m) by A48, A35, ABSVALUE:def 1;
then (osc . m) + (osc1 . m) < ((b / a) / 2) + ((b / a) / 2) by A37, A38, XREAL_1:10;
then a * ((osc . m) + (osc1 . m)) < a * (b / a) by A6, XREAL_1:70;
then A49: a * ((osc . m) + (osc1 . m)) < b by A6, XCMPLX_1:88;
osc2 . m = ((upper_sum h,T) . m) + ((- (lower_sum h,T)) . m) by SEQ_1:11
.= ((upper_sum h,T) . m) + (- ((lower_sum h,T) . m)) by SEQ_1:14
.= ((upper_sum h,T) . m) - ((lower_sum h,T) . m)
.= (upper_sum h,(T . m)) - ((lower_sum h,T) . m) by INTEGRA2:def 4
.= (upper_sum h,(T . m)) - (lower_sum h,(T . m)) by INTEGRA2:def 5
.= (Sum (upper_volume h,D)) - (lower_sum h,(T . m)) by INTEGRA1:def 9
.= (Sum (upper_volume h,D)) - (Sum (lower_volume h,D)) by INTEGRA1:def 10 ;
then A50: osc2 . m = Sum (UV2 - LV2) by RVSUM_1:120;
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;
A51: rng h is bounded_below by A5, INTEGRA1:13;
assume A52: j in dom F ; :: thesis: 0 <= F . j
j in Seg (len F) by A52, FINSEQ_1:def 3;
then A53: j in Seg (len D) by FINSEQ_1:def 18;
then A54: j in dom D by FINSEQ_1:def 3;
then A55: LV2 . j = (lower_bound (rng (h | (divset D,j)))) * (vol (divset D,j)) by INTEGRA1:def 8;
A56: ex r being Real st r in rng (h | (divset D,j))

proof

consider r being Real such that
A57: r in divset D,j by SUBSET_1:10;
j in dom D by A53, FINSEQ_1:def 3;
then divset D,j c= A by INTEGRA1:10;
then r in A by A57;
then r in dom h by FUNCT_2:def 1;
then r in (dom h) /\ (divset D,j) by A57, XBOOLE_0:def 4;
then r in dom (h | (divset D,j)) by RELAT_1:90;
then (h | (divset D,j)) . r in rng (h | (divset D,j)) by FUNCT_1:def 5;
hence ex r being Real st r in rng (h | (divset D,j)) ; :: thesis: verum

end;

rng h is bounded_above by A5, INTEGRA1:15;
then rng (h | (divset D,j)) is bounded by A51, RELAT_1:99, XXREAL_2:45;
then A58: (upper_bound (rng (h | (divset D,j)))) - (lower_bound (rng (h | (divset D,j)))) >= 0 by A56, SEQ_4:24, XREAL_1:50;
UV2 . j = (upper_bound (rng (h | (divset D,j)))) * (vol (divset D,j)) by A54, INTEGRA1:def 7;
then A59: F . j = ((upper_bound (rng (h | (divset D,j)))) * (vol (divset D,j))) - ((lower_bound (rng (h | (divset D,j)))) * (vol (divset D,j))) by A52, A55, VALUED_1:13
.= ((upper_bound (rng (h | (divset D,j)))) - (lower_bound (rng (h | (divset D,j))))) * (vol (divset D,j)) ;
vol (divset D,j) >= 0 by INTEGRA1:11;
hence 0 <= F . j by A59, A58; :: thesis: verum

end;

then osc2 . m >= 0 by A50, RVSUM_1:114;
then A60: abs (osc2 . m) = osc2 . m by ABSVALUE:def 1;
for j being Nat st j in Seg (len D) holds
(UV2 - LV2) . j <= (a * ((UV - LV) + (UV1 - LV1))) . j

proof

let j be Nat; :: thesis: ( j in Seg (len D) implies (UV2 - LV2) . j <= (a * ((UV - LV) + (UV1 - LV1))) . j )
set x = (UV2 - LV2) . j;
set y = (a * ((UV - LV) + (UV1 - LV1))) . j;
A61: (a * ((UV - LV) + (UV1 - LV1))) . j = a * (((UV - LV) + (UV1 - LV1)) . j) by RVSUM_1:67
.= a * (((UV - LV) . j) + ((UV1 - LV1) . j)) by RVSUM_1:27
.= a * (((UV . j) - (LV . j)) + ((UV1 - LV1) . j)) by RVSUM_1:48
.= a * (((UV . j) - (LV . j)) + ((UV1 . j) - (LV1 . j))) by RVSUM_1:48 ;
A62: vol (divset D,j) >= 0 by INTEGRA1:11;
assume A63: j in Seg (len D) ; :: thesis: (UV2 - LV2) . j <= (a * ((UV - LV) + (UV1 - LV1))) . j
then A64: j in dom D by FINSEQ_1:def 3;
then A65: LV2 . j = (lower_bound (rng (h | (divset D,j)))) * (vol (divset D,j)) by INTEGRA1:def 8;
UV2 . j = (upper_bound (rng (h | (divset D,j)))) * (vol (divset D,j)) by A64, INTEGRA1:def 7;
then A66: (UV2 - LV2) . j = ((upper_bound (rng (h | (divset D,j)))) * (vol (divset D,j))) - ((lower_bound (rng (h | (divset D,j)))) * (vol (divset D,j))) by A65, RVSUM_1:48
.= ((upper_bound (rng (h | (divset D,j)))) - (lower_bound (rng (h | (divset D,j))))) * (vol (divset D,j)) ;
A67: LV1 . j = (lower_bound (rng (g | (divset D,j)))) * (vol (divset D,j)) by A64, INTEGRA1:def 8;
A68: UV1 . j = (upper_bound (rng (g | (divset D,j)))) * (vol (divset D,j)) by A64, INTEGRA1:def 7;
A69: a * (((upper_bound (rng (f | (divset D,j)))) - (lower_bound (rng (f | (divset D,j))))) + ((upper_bound (rng (g | (divset D,j)))) - (lower_bound (rng (g | (divset D,j)))))) >= (upper_bound (rng (h | (divset D,j)))) - (lower_bound (rng (h | (divset D,j))))

proof

A70: j in dom D by A63, FINSEQ_1:def 3;
A71: dom (g | (divset D,j)) = (dom g) /\ (divset D,j) by RELAT_1:90
.= A /\ (divset D,j) by FUNCT_2:def 1
.= divset D,j by A70, INTEGRA1:10, XBOOLE_1:28 ;
then reconsider g1 = g | (divset D,j) as PartFunc of (divset D,j),REAL by RELSET_1:13;
reconsider g1 = g1 as Function of (divset D,j),REAL by A71, FUNCT_2:def 1;
A72: (g | (divset D,j)) | (divset D,j) is bounded_below by A3, A71, INTEGRA2:6;
A73: dom (h | (divset D,j)) = (dom h) /\ (divset D,j) by RELAT_1:90
.= A /\ (divset D,j) by FUNCT_2:def 1
.= divset D,j by A70, INTEGRA1:10, XBOOLE_1:28 ;
then reconsider h1 = h | (divset D,j) as PartFunc of (divset D,j),REAL by RELSET_1:13;
reconsider h1 = h1 as Function of (divset D,j),REAL by A73, FUNCT_2:def 1;
A74: dom (f | (divset D,j)) = (dom f) /\ (divset D,j) by RELAT_1:90
.= A /\ (divset D,j) by FUNCT_2:def 1
.= divset D,j by A70, INTEGRA1:10, XBOOLE_1:28 ;
then reconsider f1 = f | (divset D,j) as PartFunc of (divset D,j),REAL by RELSET_1:13;
A75: (f | (divset D,j)) | (divset D,j) is bounded_below by A1, A74, INTEGRA2:6;
A76: for x, y being Real st x in divset D,j & y in divset D,j holds
abs ((h1 . x) - (h1 . y)) <= a * ((abs ((f1 . x) - (f1 . y))) + (abs ((g1 . x) - (g1 . y))))

proof

let x, y be Real; :: thesis: ( x in divset D,j & y in divset D,j implies abs ((h1 . x) - (h1 . y)) <= a * ((abs ((f1 . x) - (f1 . y))) + (abs ((g1 . x) - (g1 . y)))) )
assume that
A77: x in divset D,j and
A78: y in divset D,j ; :: thesis: abs ((h1 . x) - (h1 . y)) <= a * ((abs ((f1 . x) - (f1 . y))) + (abs ((g1 . x) - (g1 . y))))
A79: g . y = g1 . y by A71, A78, FUNCT_1:70;
A80: h . y = h1 . y by A73, A78, FUNCT_1:70;
A81: h . x = h1 . x by A73, A77, FUNCT_1:70;
A82: f . y = f1 . y by A74, A78, FUNCT_1:70;
A83: f . x = f1 . x by A74, A77, FUNCT_1:70;
g . x = g1 . x by A71, A77, FUNCT_1:70;
hence abs ((h1 . x) - (h1 . y)) <= a * ((abs ((f1 . x) - (f1 . y))) + (abs ((g1 . x) - (g1 . y)))) by A7, A74, A77, A78, A79, A83, A82, A81, A80; :: thesis: verum

end;

(g | (divset D,j)) | (divset D,j) is bounded_above by A3, A71, INTEGRA2:5;
then A84: g1 | (divset D,j) is bounded by A72;
(f | (divset D,j)) | (divset D,j) is bounded_above by A1, A74, INTEGRA2:5;
then A85: f1 | (divset D,j) is bounded by A75;
f1 is total by A74, PARTFUN1:def 4;
hence a * (((upper_bound (rng (f | (divset D,j)))) - (lower_bound (rng (f | (divset D,j))))) + ((upper_bound (rng (g | (divset D,j)))) - (lower_bound (rng (g | (divset D,j)))))) >= (upper_bound (rng (h | (divset D,j)))) - (lower_bound (rng (h | (divset D,j)))) by A6, A85, A84, A76, Th26; :: thesis: verum

end;

LV . j = (lower_bound (rng (f | (divset D,j)))) * (vol (divset D,j)) by A64, INTEGRA1:def 8;
then (a * ((UV - LV) + (UV1 - LV1))) . j = a * ((((upper_bound (rng (f | (divset D,j)))) * (vol (divset D,j))) - ((lower_bound (rng (f | (divset D,j)))) * (vol (divset D,j)))) + (((upper_bound (rng (g | (divset D,j)))) * (vol (divset D,j))) - ((lower_bound (rng (g | (divset D,j)))) * (vol (divset D,j))))) by A64, A68, A67, A61, INTEGRA1:def 7
.= (a * (((upper_bound (rng (f | (divset D,j)))) - (lower_bound (rng (f | (divset D,j))))) + ((upper_bound (rng (g | (divset D,j)))) - (lower_bound (rng (g | (divset D,j))))))) * (vol (divset D,j)) ;
hence (UV2 - LV2) . j <= (a * ((UV - LV) + (UV1 - LV1))) . j by A66, A69, A62, XREAL_1:66; :: thesis: verum

end;

then osc2 . m <= Sum (a * ((UV - LV) + (UV1 - LV1))) by A50, RVSUM_1:112;
then osc2 . m <= a * (Sum ((UV - LV) + (UV1 - LV1))) by RVSUM_1:117;
then osc2 . m <= a * ((osc . m) + (osc1 . m)) by A24, A25, RVSUM_1:119;
hence abs ((osc2 . m) - 0 ) < b by A60, A49, 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 ((osc2 . m) - 0 ) < b ; :: thesis: verum

end;

then osc2 is convergent by SEQ_2:def 6;
then A86: lim ((upper_sum h,T) - (lower_sum h,T)) = 0 by A18, SEQ_2:def 7;
A87: lower_sum h,T is convergent by A5, A8, A9, Th8;
upper_sum h,T is convergent by A5, A8, A9, Th9;
hence (lim (upper_sum h,T)) - (lim (lower_sum h,T)) = 0 by A87, A86, SEQ_2:26; :: thesis: verum

end;

hence h is integrable by A5, Th12; :: thesis: verum