let a be Real; :: thesis: for A being non empty 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
|.((g . x) - (g . y)).| <= a * |.((f . x) - (f . y)).| ) holds
g is integrable
let A be non empty 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
|.((g . x) - (g . y)).| <= a * |.((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
|.((g . x) - (g . y)).| <= a * |.((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
|.((g . x) - (g . y)).| <= a * |.((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;
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:12;
A12: for b being Real st 0 < b holds
ex n being Nat st
for m being Nat st n <= m holds
|.((osc1 . m) - 0).| < b

proof

let b be Real; :: thesis: ( 0 < b implies ex n being Nat st
for m being Nat st n <= m holds
|.((osc1 . m) - 0).| < b )
assume b > 0 ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((osc1 . m) - 0).| < b
then b / a > 0 by A4, XREAL_1:139;
then consider n being Nat such that
A13: for m being Nat st n <= m holds
|.((osc . m) - 0).| < b / a by A10, A11, SEQ_2:def 7;
take n ; :: thesis: for m being Nat st n <= m holds
|.((osc1 . m) - 0).| < b
let m be Nat; :: thesis: ( n <= m implies |.((osc1 . m) - 0).| < b )
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;
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 A14: osc . m = Sum (UV - LV) by RVSUM_1:90;
assume n <= m ; :: thesis: |.((osc1 . m) - 0).| < b
then A15: |.((osc . m) - 0).| < b / a by A13;
len (lower_volume (g,D)) = len D by INTEGRA1:def 7;
then reconsider LV1 = lower_volume (g,D) as Element of (len D) -tuples_on REAL by FINSEQ_2:133;
len (upper_volume (g,D)) = len D by INTEGRA1:def 6;
then reconsider UV1 = upper_volume (g,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 (g,T)) . m) + ((- (lower_sum (g,T))) . m) by SEQ_1:7
.= ((upper_sum (g,T)) . m) + (- ((lower_sum (g,T)) . m)) by SEQ_1:10
.= ((upper_sum (g,T)) . m) - ((lower_sum (g,T)) . m)
.= (upper_sum (g,(T . mm))) - ((lower_sum (g,T)) . m) by INTEGRA2:def 2
.= (upper_sum (g,(T . mm))) - (lower_sum (g,(T . mm))) by INTEGRA2:def 3
.= (Sum (upper_volume (g,D))) - (lower_sum (g,(T . mm))) by INTEGRA1:def 8
.= (Sum (upper_volume (g,D))) - (Sum (lower_volume (g,D))) by INTEGRA1:def 9 ;
then A16: osc1 . m = Sum (UV1 - LV1) by RVSUM_1:90;
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:11;
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 CARD_1:def 7;
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 7;
A22: ex r being Real st r in rng (g | (divset (D,j)))

proof

consider r being Element of REAL such that
A23: r in divset (D,j) by SUBSET_1:4;
j in dom D by A19, FINSEQ_1:def 3;
then divset (D,j) c= A by INTEGRA1:8;
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:61;
then (g | (divset (D,j))) . r in rng (g | (divset (D,j))) by FUNCT_1:def 3;
hence ex r being Real st r in rng (g | (divset (D,j))) ; :: thesis: verum

end;

rng g is bounded_above by A3, INTEGRA1:13;
then rng (g | (divset (D,j))) is real-bounded by A17, RELAT_1:70, XXREAL_2:45;
then A24: (upper_bound (rng (g | (divset (D,j))))) - (lower_bound (rng (g | (divset (D,j))))) >= 0 by A22, SEQ_4:11, XREAL_1:48;
UV1 . j = (upper_bound (rng (g | (divset (D,j))))) * (vol (divset (D,j))) by A20, INTEGRA1:def 6;
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:9;
hence 0 <= F . j by A25, A24; :: thesis: verum

end;

then A26: osc1 . m >= 0 by A16, RVSUM_1:84;
then A27: |.(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:45;
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 7;
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:8, INTEGRA2:6;
A35: dom (g | (divset (D,j))) = (dom g) /\ (divset (D,j)) by RELAT_1:61
.= A /\ (divset (D,j)) by FUNCT_2:def 1
.= divset (D,j) by A33, INTEGRA1:8, XBOOLE_1:28 ;
then reconsider g1 = g | (divset (D,j)) as PartFunc of (divset (D,j)),REAL by RELSET_1:5;
A36: dom (f | (divset (D,j))) = (dom f) /\ (divset (D,j)) by RELAT_1:61
.= A /\ (divset (D,j)) by FUNCT_2:def 1
.= divset (D,j) by A33, INTEGRA1:8, XBOOLE_1:28 ;
then reconsider f1 = f | (divset (D,j)) as PartFunc of (divset (D,j)),REAL by RELSET_1:5;
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:8;
A38: for x, y being Real st x in divset (D,j) & y in divset (D,j) holds
|.((g1 . x) - (g1 . y)).| <= a * |.((f1 . x) - (f1 . y)).|

proof

let x, y be Real; :: thesis: ( x in divset (D,j) & y in divset (D,j) implies |.((g1 . x) - (g1 . y)).| <= a * |.((f1 . x) - (f1 . y)).| )
assume that
A39: x in divset (D,j) and
A40: y in divset (D,j) ; :: thesis: |.((g1 . x) - (g1 . y)).| <= a * |.((f1 . x) - (f1 . y)).|
A41: g . y = g1 . y by A35, A40, FUNCT_1:47;
A42: f . y = f1 . y by A36, A40, FUNCT_1:47;
A43: f . x = f1 . x by A36, A39, FUNCT_1:47;
g . x = g1 . x by A35, A39, FUNCT_1:47;
hence |.((g1 . x) - (g1 . y)).| <= a * |.((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:8, 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:9;
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:64;
UV1 . j = (upper_bound (rng (g | (divset (D,j))))) * (vol (divset (D,j))) by A30, INTEGRA1:def 6;
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:27
.= ((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 7;
UV . j = (upper_bound (rng (f | (divset (D,j))))) * (vol (divset (D,j))) by A30, INTEGRA1:def 6;
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:27
.= 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:82;
then A47: osc1 . m <= a * (osc . m) by A14, RVSUM_1:87;
then osc . m >= 0 / a by A4, A26, XREAL_1:79;
then |.(osc . m).| = osc . m by ABSVALUE:def 1;
then a * (osc . m) < a * (b / a) by A4, A15, XREAL_1:68;
then a * (osc . m) < b by A4, XCMPLX_1:87;
hence |.((osc1 . m) - 0).| < b by A47, A27, XXREAL_0:2; :: 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:12; :: thesis: verum

end;

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