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

proof

let T be DivSequence of A; :: thesis:
assume that
A6: delta T is convergent and
A7: lim (delta T) = 0 ; :: thesis:
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, SEQ_2:25;
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 ;
(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:26;
A12: 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 ((osc1 . m) - 0 ) < b

proof

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

proof

let m be Element of NAT ; :: thesis:
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 A14: osc . m = Sum (UV - LV) by RVSUM_1:120;
assume n <= m ; :: thesis:
then A15: abs ((osc . m) - 0 ) < b / a by A13;
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 F = UV1 - LV1 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 A16: osc1 . m = Sum (UV1 - LV1) by RVSUM_1:120;
for j being Nat st j in dom F holds
0 <= F . j

proof

let j be Nat; :: thesis:
set r = F . j;
A17: rng g is bounded_below by A3, INTEGRA1:13;
assume A18: j in dom F ; :: thesis:
j in Seg (len F) by A18, FINSEQ_1:def 3;
then A19: j in Seg (len D) by FINSEQ_1:def 18;
then A20: j in dom D by FINSEQ_1:def 3;
then A21: LV1 . j = (lower_bound (rng (g | (divset D,j)))) * (vol (divset D,j)) by INTEGRA1:def 8;
A22: ex r being Real st r in rng (g | (divset D,j))

proof

consider r being Real such that
A23: 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 A23;
then r in dom g by FUNCT_2:def 1;
then r in (dom g) /\ (divset D,j) by A23, 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:

end;

rng g is bounded_above by A3, INTEGRA1:15;
then rng (g | (divset D,j)) is bounded by A17, RELAT_1:99, XXREAL_2:45;
then A24: (upper_bound (rng (g | (divset D,j)))) - (lower_bound (rng (g | (divset D,j)))) >= 0 by A22, SEQ_4:24, XREAL_1:50;
UV1 . j = (upper_bound (rng (g | (divset D,j)))) * (vol (divset D,j)) by A20, INTEGRA1:def 7;
then A25: F . j = ((upper_bound (rng (g | (divset D,j)))) * (vol (divset D,j))) - ((lower_bound (rng (g | (divset D,j)))) * (vol (divset D,j))) by A18, A21, 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 <= F . j by A25, A24; :: thesis:

end;

then A26: osc1 . m >= 0 by A16, RVSUM_1:114;
then A27: abs (osc1 . m) = osc1 . m by ABSVALUE:def 1;
for j being Nat st j in Seg (len D) holds
(UV1 - LV1) . j <= (a * (UV - LV)) . j

proof

let j be Nat; :: thesis:
set x = (UV1 - LV1) . j;
set y = (a * (UV - LV)) . j;
A28: (a * (UV - LV)) . j = a * ((UV - LV) . j) by RVSUM_1:67;
assume A29: j in Seg (len D) ; :: thesis:
then A30: j in dom D by FINSEQ_1:def 3;
then A31: LV1 . j = (lower_bound (rng (g | (divset D,j)))) * (vol (divset D,j)) by INTEGRA1:def 8;
A32: 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))))

proof

A33: j in dom D by A29, FINSEQ_1:def 3;
then A34: (f | (divset D,j)) | (divset D,j) is bounded_below by A1, INTEGRA1:10, INTEGRA2:6;
A35: 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 A33, INTEGRA1:10, XBOOLE_1:28 ;
then reconsider g1 = g | (divset D,j) as PartFunc of (divset D,j),REAL by RELSET_1:13;
A36: 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 A33, INTEGRA1:10, XBOOLE_1:28 ;
then reconsider f1 = f | (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 A35, FUNCT_2:def 1;
reconsider f1 = f1 as Function of (divset D,j),REAL by A36, FUNCT_2:def 1;
A37: divset D,j c= A by A33, INTEGRA1:10;
A38: for x, y being Real st x in divset D,j & y in divset D,j holds
abs ((g1 . x) - (g1 . y)) <= a * (abs ((f1 . x) - (f1 . y)))

proof

let x, y be Real; :: thesis:
assume that
A39: x in divset D,j and
A40: y in divset D,j ; :: thesis:
A41: g . y = g1 . y by A35, A40, FUNCT_1:70;
A42: f . y = f1 . y by A36, A40, FUNCT_1:70;
A43: f . x = f1 . x by A36, A39, FUNCT_1:70;
g . x = g1 . x by A35, A39, FUNCT_1:70;
hence abs ((g1 . x) - (g1 . y)) <= a * (abs ((f1 . x) - (f1 . y))) by A5, A37, A39, A40, A41, A43, A42; :: thesis:

end;

end;

end;

then osc1 . m <= Sum (a * (UV - LV)) by A16, RVSUM_1:112;
then A47: osc1 . m <= a * (osc . m) by A14, RVSUM_1:117;
then osc . m >= 0 / a by A4, A26, XREAL_1:81;
then abs (osc . m) = osc . m by ABSVALUE:def 1;
then a * (osc . m) < a * (b / a) by A4, A15, XREAL_1:70;
then a * (osc . m) < b by A4, XCMPLX_1:88;
hence abs ((osc1 . m) - 0 ) < b by A47, A27, XXREAL_0:2; :: thesis:

end;

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

end;

then osc1 is convergent by SEQ_2:def 6;
then A48: lim ((upper_sum g,T) - (lower_sum g,T)) = 0 by A12, SEQ_2:def 7;
A49: lower_sum g,T is convergent by A3, A6, A7, Th8;
upper_sum g,T is convergent by A3, A6, A7, Th9;
hence (lim (upper_sum g,T)) - (lim (lower_sum g,T)) = 0 by A49, A48, SEQ_2:26; :: thesis:

end;

hence g is integrable by A3, Th12; :: thesis: