let a be Real; :: thesis: for A being non empty 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
|.((h . x) - (h . y)).| <= a * (|.((f . x) - (f . y)).| + |.((g . x) - (g . y)).|) ) holds
h is integrable
let A be non empty 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
|.((h . x) - (h . y)).| <= a * (|.((f . x) - (f . y)).| + |.((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
|.((h . x) - (h . y)).| <= a * (|.((f . x) - (f . y)).| + |.((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
|.((h . x) - (h . y)).| <= a * (|.((f . x) - (f . y)).| + |.((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;
(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:12;
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:12;
A17: (upper_sum (f,T)) - (lower_sum (f,T)) is convergent by A15, A14;
A18: for b being Real st 0 < b holds
ex n being Nat st
for m being Nat st n <= m holds
|.((osc2 . 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
|.((osc2 . m) - 0).| < b )
assume b > 0 ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((osc2 . m) - 0).| < b
then b / a > 0 by A6, XREAL_1:139;
then A19: (b / a) / 2 > 0 by XREAL_1:139;
then consider n1 being Nat such that
A20: for m being Nat st n1 <= m holds
|.((osc . m) - 0).| < (b / a) / 2 by A17, A16, SEQ_2:def 7;
consider n2 being Nat such that
A21: for m being Nat st n2 <= m holds
|.((osc1 . m) - 0).| < (b / a) / 2 by A12, A13, A19, SEQ_2:def 7;
ex n being Nat st
( n1 <= n & n2 <= n )
proof
take n = max (n1,n2); :: thesis: ( n is Nat & n1 <= n & n2 <= n )
n is Element of NAT by ORDINAL1:def 12;
hence ( n is Nat & n1 <= n & n2 <= n ) by XXREAL_0:25; :: thesis: verum
end;
then consider n being Nat such that
A22: n1 <= n and
A23: n2 <= n ;
take n ; :: thesis: for m being Nat st n <= m holds
|.((osc2 . m) - 0).| < b
let m be Nat; :: thesis: ( n <= m implies |.((osc2 . 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 A24: osc . m = Sum (UV - LV) by RVSUM_1:90;
len (lower_volume (h,D)) = len D by INTEGRA1:def 7;
then reconsider LV2 = lower_volume (h,D) as Element of (len D) -tuples_on REAL by FINSEQ_2:133;
len (upper_volume (h,D)) = len D by INTEGRA1:def 6;
then reconsider UV2 = upper_volume (h,D) as Element of (len D) -tuples_on REAL by FINSEQ_2:133;
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 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: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 A25: osc1 . m = Sum (UV1 - LV1) by RVSUM_1:90;
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:11;
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 CARD_1:def 7;
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 7;
A31: ex r being Real st r in rng (g | (divset (D,j)))
proof
consider r being Element of REAL such that
A32: r in divset (D,j) by SUBSET_1:4;
j in dom D by A28, FINSEQ_1:def 3;
then divset (D,j) c= A by INTEGRA1:8;
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: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 A26, RELAT_1:70, XXREAL_2:45;
then A33: (upper_bound (rng (g | (divset (D,j))))) - (lower_bound (rng (g | (divset (D,j))))) >= 0 by A31, SEQ_4:11, XREAL_1:48;
UV1 . j = (upper_bound (rng (g | (divset (D,j))))) * (vol (divset (D,j))) by A29, INTEGRA1:def 6;
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:9;
hence 0 <= G . j by A34, A33; :: thesis: verum
end;
then A35: osc1 . m >= 0 by A25, RVSUM_1:84;
assume A36: n <= m ; :: thesis: |.((osc2 . m) - 0).| < b
then n1 <= m by A22, XXREAL_0:2;
then A37: |.((osc . m) - 0).| < (b / a) / 2 by A20;
n2 <= m by A23, A36, XXREAL_0:2;
then A38: |.((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:11;
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 CARD_1:def 7;
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 7;
A44: ex r being Real st r in rng (f | (divset (D,j)))
proof
consider r being Element of REAL such that
A45: r in divset (D,j) by SUBSET_1:4;
j in dom D by A41, FINSEQ_1:def 3;
then divset (D,j) c= A by INTEGRA1:8;
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:61;
then (f | (divset (D,j))) . r in rng (f | (divset (D,j))) by FUNCT_1:def 3;
hence ex r being Real st r in rng (f | (divset (D,j))) ; :: thesis: verum
end;
rng f is bounded_above by A1, INTEGRA1:13;
then rng (f | (divset (D,j))) is real-bounded by A39, RELAT_1:70, XXREAL_2:45;
then A46: (upper_bound (rng (f | (divset (D,j))))) - (lower_bound (rng (f | (divset (D,j))))) >= 0 by A44, SEQ_4:11, XREAL_1:48;
UV . j = (upper_bound (rng (f | (divset (D,j))))) * (vol (divset (D,j))) by A42, INTEGRA1:def 6;
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:9;
hence 0 <= H . j by A47, A46; :: thesis: verum
end;
then A48: osc . m >= 0 by A24, RVSUM_1:84;
then (osc . m) * (osc1 . m) >= 0 by A35;
then |.(osc . m).| + |.(osc1 . m).| = |.((osc . m) + (osc1 . m)).| by ABSVALUE:11;
then |.((osc . m) - 0).| + |.(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:8;
then a * ((osc . m) + (osc1 . m)) < a * (b / a) by A6, XREAL_1:68;
then A49: a * ((osc . m) + (osc1 . m)) < b by A6, XCMPLX_1:87;
osc2 . m = ((upper_sum (h,T)) . m) + ((- (lower_sum (h,T))) . m) by SEQ_1:7
.= ((upper_sum (h,T)) . m) + (- ((lower_sum (h,T)) . m)) by SEQ_1:10
.= ((upper_sum (h,T)) . m) - ((lower_sum (h,T)) . m)
.= (upper_sum (h,(T . mm))) - ((lower_sum (h,T)) . m) by INTEGRA2:def 2
.= (upper_sum (h,(T . mm))) - (lower_sum (h,(T . mm))) by INTEGRA2:def 3
.= (Sum (upper_volume (h,D))) - (lower_sum (h,(T . mm))) by INTEGRA1:def 8
.= (Sum (upper_volume (h,D))) - (Sum (lower_volume (h,D))) by INTEGRA1:def 9 ;
then A50: osc2 . m = Sum (UV2 - LV2) 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;
A51: rng h is bounded_below by A5, INTEGRA1:11;
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 CARD_1:def 7;
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 7;
A56: ex r being Real st r in rng (h | (divset (D,j)))
proof
consider r being Element of REAL such that
A57: r in divset (D,j) by SUBSET_1:4;
j in dom D by A53, FINSEQ_1:def 3;
then divset (D,j) c= A by INTEGRA1:8;
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:61;
then (h | (divset (D,j))) . r in rng (h | (divset (D,j))) by FUNCT_1:def 3;
hence ex r being Real st r in rng (h | (divset (D,j))) ; :: thesis: verum
end;
rng h is bounded_above by A5, INTEGRA1:13;
then rng (h | (divset (D,j))) is real-bounded by A51, RELAT_1:70, XXREAL_2:45;
then A58: (upper_bound (rng (h | (divset (D,j))))) - (lower_bound (rng (h | (divset (D,j))))) >= 0 by A56, SEQ_4:11, XREAL_1:48;
UV2 . j = (upper_bound (rng (h | (divset (D,j))))) * (vol (divset (D,j))) by A54, INTEGRA1:def 6;
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:9;
hence 0 <= F . j by A59, A58; :: thesis: verum
end;
then osc2 . m >= 0 by A50, RVSUM_1:84;
then A60: |.(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:45
.= a * (((UV - LV) . j) + ((UV1 - LV1) . j)) by RVSUM_1:11
.= a * (((UV . j) - (LV . j)) + ((UV1 - LV1) . j)) by RVSUM_1:27
.= a * (((UV . j) - (LV . j)) + ((UV1 . j) - (LV1 . j))) by RVSUM_1:27 ;
A62: vol (divset (D,j)) >= 0 by INTEGRA1:9;
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 7;
UV2 . j = (upper_bound (rng (h | (divset (D,j))))) * (vol (divset (D,j))) by A64, INTEGRA1:def 6;
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:27
.= ((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 7;
A68: UV1 . j = (upper_bound (rng (g | (divset (D,j))))) * (vol (divset (D,j))) by A64, INTEGRA1:def 6;
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:61
.= A /\ (divset (D,j)) by FUNCT_2:def 1
.= divset (D,j) by A70, INTEGRA1:8, XBOOLE_1:28 ;
then reconsider g1 = g | (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 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:61
.= A /\ (divset (D,j)) by FUNCT_2:def 1
.= divset (D,j) by A70, INTEGRA1:8, XBOOLE_1:28 ;
then reconsider h1 = h | (divset (D,j)) as PartFunc of (divset (D,j)),REAL by RELSET_1:5;
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:61
.= A /\ (divset (D,j)) by FUNCT_2:def 1
.= divset (D,j) by A70, INTEGRA1:8, XBOOLE_1:28 ;
then reconsider f1 = f | (divset (D,j)) as PartFunc of (divset (D,j)),REAL by RELSET_1:5;
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
|.((h1 . x) - (h1 . y)).| <= a * (|.((f1 . x) - (f1 . y)).| + |.((g1 . x) - (g1 . y)).|)
proof
let x, y be Real; :: thesis: ( x in divset (D,j) & y in divset (D,j) implies |.((h1 . x) - (h1 . y)).| <= a * (|.((f1 . x) - (f1 . y)).| + |.((g1 . x) - (g1 . y)).|) )
assume that
A77: x in divset (D,j) and
A78: y in divset (D,j) ; :: thesis: |.((h1 . x) - (h1 . y)).| <= a * (|.((f1 . x) - (f1 . y)).| + |.((g1 . x) - (g1 . y)).|)
A79: g . y = g1 . y by A71, A78, FUNCT_1:47;
A80: h . y = h1 . y by A73, A78, FUNCT_1:47;
A81: h . x = h1 . x by A73, A77, FUNCT_1:47;
A82: f . y = f1 . y by A74, A78, FUNCT_1:47;
A83: f . x = f1 . x by A74, A77, FUNCT_1:47;
g . x = g1 . x by A71, A77, FUNCT_1:47;
hence |.((h1 . x) - (h1 . y)).| <= a * (|.((f1 . x) - (f1 . y)).| + |.((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 2;
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 7;
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 6
.= (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:64; :: thesis: verum
end;
then osc2 . m <= Sum (a * ((UV - LV) + (UV1 - LV1))) by A50, RVSUM_1:82;
then osc2 . m <= a * (Sum ((UV - LV) + (UV1 - LV1))) by RVSUM_1:87;
then osc2 . m <= a * ((osc . m) + (osc1 . m)) by A24, A25, RVSUM_1:89;
hence |.((osc2 . m) - 0).| < b by A60, A49, XXREAL_0:2; :: 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:12; :: thesis: verum
end;
hence h is integrable by A5, Th12; :: thesis: verum