let a be Real; :: thesis: for A being closed-interval Subset of REAL
for f, g being Function of A,REAL st f | A is bounded & f is integrable & g | A is bounded & a > 0 & ( for x, y being Real st x in A & y in A holds
abs ((g . x) - (g . y)) <= a * (abs ((f . x) - (f . y))) ) holds
g is integrable
let A be closed-interval Subset of REAL; :: thesis: for f, g being Function of A,REAL st f | A is bounded & f is integrable & g | A is bounded & a > 0 & ( for x, y being Real st x in A & y in A holds
abs ((g . x) - (g . y)) <= a * (abs ((f . x) - (f . y))) ) holds
g is integrable
let f, g be Function of A,REAL; :: thesis: ( f | A is bounded & f is integrable & g | A is bounded & a > 0 & ( for x, y being Real st x in A & y in A holds
abs ((g . x) - (g . y)) <= a * (abs ((f . x) - (f . y))) ) implies g is integrable )
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: g is integrable
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: ( delta T is convergent & lim (delta T) = 0 implies (lim (upper_sum (g,T))) - (lim (lower_sum (g,T))) = 0 )
assume that
A6: delta T is convergent and
A7: lim (delta T) = 0 ; :: thesis: (lim (upper_sum (g,T))) - (lim (lower_sum (g,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, 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: ( 0 < b implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((osc1 . 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 ((osc1 . m) - 0) < b
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: ( n <= m implies abs ((osc1 . 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 A14: osc . m = Sum (UV - LV) by RVSUM_1:120;
assume n <= m ; :: thesis: abs ((osc1 . m) - 0) < b
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: ( j in dom F implies 0 <= F . j )
set r = F . j;
A17: rng g is bounded_below by A3, INTEGRA1:13;
assume A18: j in dom F ; :: thesis: 0 <= F . j
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: verum

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: verum

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: ( j in Seg (len D) implies (UV1 - LV1) . j <= (a * (UV - LV)) . j )
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: (UV1 - LV1) . j <= (a * (UV - LV)) . j
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: ( x in divset (D,j) & y in divset (D,j) implies abs ((g1 . x) - (g1 . y)) <= a * (abs ((f1 . x) - (f1 . y))) )
assume that
A39: x in divset (D,j) and
A40: y in divset (D,j) ; :: thesis: abs ((g1 . x) - (g1 . y)) <= a * (abs ((f1 . x) - (f1 . y)))
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: verum

end;

(f | (divset (D,j))) | (divset (D,j)) is bounded_above by A1, A33, INTEGRA1:10, INTEGRA2:5;
then f1 | (divset (D,j)) is bounded by A34;
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))))) by A4, A38, Th25; :: thesis: verum

end;

vol (divset (D,j)) >= 0 by INTEGRA1:11;
then A44: (a * ((upper_bound (rng (f | (divset (D,j))))) - (lower_bound (rng (f | (divset (D,j))))))) * (vol (divset (D,j))) >= ((upper_bound (rng (g | (divset (D,j))))) - (lower_bound (rng (g | (divset (D,j)))))) * (vol (divset (D,j))) by A32, XREAL_1:66;
UV1 . j = (upper_bound (rng (g | (divset (D,j))))) * (vol (divset (D,j))) by A30, INTEGRA1:def 7;
then A45: (UV1 - LV1) . j = ((upper_bound (rng (g | (divset (D,j))))) * (vol (divset (D,j)))) - ((lower_bound (rng (g | (divset (D,j))))) * (vol (divset (D,j)))) by A31, RVSUM_1:48
.= ((upper_bound (rng (g | (divset (D,j))))) - (lower_bound (rng (g | (divset (D,j)))))) * (vol (divset (D,j))) ;
A46: LV . j = (lower_bound (rng (f | (divset (D,j))))) * (vol (divset (D,j))) by A30, INTEGRA1:def 8;
UV . j = (upper_bound (rng (f | (divset (D,j))))) * (vol (divset (D,j))) by A30, INTEGRA1:def 7;
then (a * (UV - LV)) . j = a * (((upper_bound (rng (f | (divset (D,j))))) * (vol (divset (D,j)))) - ((lower_bound (rng (f | (divset (D,j))))) * (vol (divset (D,j))))) by A46, A28, RVSUM_1:48
.= a * (((upper_bound (rng (f | (divset (D,j))))) - (lower_bound (rng (f | (divset (D,j)))))) * (vol (divset (D,j)))) ;
hence (UV1 - LV1) . j <= (a * (UV - LV)) . j by A45, A44; :: thesis: verum

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: verum

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: verum

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: verum

end;

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