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: ( upper_sum g,T is convergent & lower_sum g,T is convergent ) by A3, A8, A9, Th8, Th9;
A11: ( upper_sum f,T is convergent & lower_sum f,T is convergent ) by A1, A8, A9, Th8, Th9;
A12: ( upper_sum h,T is convergent & lower_sum h,T is convergent ) by A5, A8, A9, Th8, Th9;
A13: (lim (upper_sum f,T)) - (lim (lower_sum f,T)) = 0 by A1, A2, A8, A9, Th12;
A14: (lim (upper_sum g,T)) - (lim (lower_sum g,T)) = 0 by A3, A4, A8, A9, Th12;
A15: (upper_sum f,T) - (lower_sum f,T) is convergent by A11, SEQ_2:25;
A16: (upper_sum g,T) - (lower_sum g,T) is convergent by A10, SEQ_2:25;
reconsider osc = (upper_sum f,T) - (lower_sum f,T) as Real_Sequence ;
reconsider osc1 = (upper_sum g,T) - (lower_sum g,T) as Real_Sequence ;
reconsider osc2 = (upper_sum h,T) - (lower_sum h,T) as Real_Sequence ;
A17: lim ((upper_sum f,T) - (lower_sum f,T)) = 0 by A11, A13, SEQ_2:26;
A18: lim ((upper_sum g,T) - (lower_sum g,T)) = 0 by A10, A14, SEQ_2:26;
A19: 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 A20: (b / a) / 2 > 0 by XREAL_1:141;
then consider n1 being Element of NAT such that
A21: for m being Element of NAT st n1 <= m holds
abs ((osc . m) - 0 ) < (b / a) / 2 by A15, A17, SEQ_2:def 7;
consider n2 being Element of NAT such that
A22: for m being Element of NAT st n2 <= m holds
abs ((osc1 . m) - 0 ) < (b / a) / 2 by A16, A18, A20, 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 & n2 <= n ) by XXREAL_0:25;
hence ( n is Element of REAL & n is Element of NAT & n1 <= n & n2 <= n ) ; :: thesis: verum

end;

then consider n being Element of NAT such that
A23: ( n1 <= n & 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 )
assume n <= m ; :: thesis: abs ((osc2 . m) - 0 ) < b
then ( n1 <= m & n2 <= m ) by A23, XXREAL_0:2;
then A24: ( abs ((osc . m) - 0 ) < (b / a) / 2 & abs ((osc1 . m) - 0 ) < (b / a) / 2 ) by A21, A22;
reconsider D = T . m as Division of A ;
A25: 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 ;
A26: 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 ;
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 CATALG_1:5;
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 CATALG_1:5;
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 CATALG_1:5;
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 CATALG_1:5;
A27: osc . m = Sum (UV - LV) by A25, RVSUM_1:120;
A28: osc1 . m = Sum (UV1 - LV1) by A26, RVSUM_1:120;
A29: 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 ;
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 CATALG_1:5;
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 CATALG_1:5;
A30: osc2 . m = Sum (UV2 - LV2) by A29, RVSUM_1:120;
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 )
assume A31: j in Seg (len D) ; :: thesis: (UV2 - LV2) . j <= (a * ((UV - LV) + (UV1 - LV1))) . j
then B31: j in dom D by FINSEQ_1:def 3;
set x = (UV2 - LV2) . j;
set y = (a * ((UV - LV) + (UV1 - LV1))) . j;
A32: UV2 . j = (upper_bound (rng (h | (divset D,j)))) * (vol (divset D,j)) by B31, INTEGRA1:def 7;
LV2 . j = (lower_bound (rng (h | (divset D,j)))) * (vol (divset D,j)) by B31, INTEGRA1:def 8;
then A33: (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 A32, RVSUM_1:48
.= ((upper_bound (rng (h | (divset D,j)))) - (lower_bound (rng (h | (divset D,j))))) * (vol (divset D,j)) ;
A34: LV . j = (lower_bound (rng (f | (divset D,j)))) * (vol (divset D,j)) by B31, INTEGRA1:def 8;
A35: UV1 . j = (upper_bound (rng (g | (divset D,j)))) * (vol (divset D,j)) by B31, INTEGRA1:def 7;
A36: LV1 . j = (lower_bound (rng (g | (divset D,j)))) * (vol (divset D,j)) by B31, INTEGRA1:def 8;
(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 ;
then A37: (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 A34, A35, A36, B31, 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)) ;
A38: 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

A39: j in dom D by A31, FINSEQ_1:def 3;
A40: 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 A39, INTEGRA1:10, XBOOLE_1:28 ;
then reconsider f1 = f | (divset D,j) as PartFunc of (divset D,j),REAL by RELSET_1:13;
A41: 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 A39, 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 A41, FUNCT_2:def 1;
A42: 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 A39, 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 A42, FUNCT_2:def 1;
( f | A is bounded_above & f | A is bounded_below ) by A1;
then ( (f | (divset D,j)) | (divset D,j) is bounded_above & (f | (divset D,j)) | (divset D,j) is bounded_below ) by A40, INTEGRA2:5, INTEGRA2:6;
then (f | (divset D,j)) | (divset D,j) is bounded ;
then consider r1 being real number such that
A43: for x being set st x in (divset D,j) /\ (dom (f | (divset D,j))) holds
abs ((f | (divset D,j)) . x) <= r1 by RFUNCT_1:90;
( g | A is bounded_above & g | A is bounded_below ) by A3;
then ( (g | (divset D,j)) | (divset D,j) is bounded_above & (g | (divset D,j)) | (divset D,j) is bounded_below ) by A41, INTEGRA2:5, INTEGRA2:6;
then (g | (divset D,j)) | (divset D,j) is bounded ;
then consider r2 being real number such that
A44: for x being set st x in (divset D,j) /\ (dom (g | (divset D,j))) holds
abs ((g | (divset D,j)) . x) <= r2 by RFUNCT_1:90;
A45: f1 | (divset D,j) is bounded by A43, RFUNCT_1:90;
A46: g1 | (divset D,j) is bounded by A44, RFUNCT_1:90;
( f1 is total & g1 is total & h1 is total ) by A40, PARTFUN1:def 4;
then A47: ( f1 is Function of (divset D,j),REAL & g1 is Function of (divset D,j),REAL & h1 is Function of (divset D,j),REAL ) ;
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 A48: ( x in divset D,j & y in divset D,j ) ; :: thesis: abs ((h1 . x) - (h1 . y)) <= a * ((abs ((f1 . x) - (f1 . y))) + (abs ((g1 . x) - (g1 . y))))
then ( g . x = g1 . x & g . y = g1 . y & f . x = f1 . x & f . y = f1 . y & h . x = h1 . x & h . y = h1 . y ) by A40, A41, A42, FUNCT_1:70;
hence abs ((h1 . x) - (h1 . y)) <= a * ((abs ((f1 . x) - (f1 . y))) + (abs ((g1 . x) - (g1 . y)))) by A7, A40, A48; :: thesis: verum

end;

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, A45, A46, A47, Th26; :: thesis: verum

end;

vol (divset D,j) >= 0 by INTEGRA1:11;
hence (UV2 - LV2) . j <= (a * ((UV - LV) + (UV1 - LV1))) . j by A33, A37, A38, XREAL_1:66; :: thesis: verum

end;

then osc2 . m <= Sum (a * ((UV - LV) + (UV1 - LV1))) by A30, RVSUM_1:112;
then osc2 . m <= a * (Sum ((UV - LV) + (UV1 - LV1))) by RVSUM_1:117;
then A49: osc2 . m <= a * ((osc . m) + (osc1 . m)) by A27, A28, RVSUM_1:119;
reconsider F = UV2 - LV2 as FinSequence of REAL ;
osc2 . m >= 0

proof

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 )
assume A50: j in dom F ; :: thesis: 0 <= F . j
set r = F . j;
j in Seg (len F) by A50, FINSEQ_1:def 3;
then A51: j in Seg (len D) by FINSEQ_1:def 18;
then j in dom D by FINSEQ_1:def 3;
then ( UV2 . j = (upper_bound (rng (h | (divset D,j)))) * (vol (divset D,j)) & LV2 . j = (lower_bound (rng (h | (divset D,j)))) * (vol (divset D,j)) ) by INTEGRA1:def 7, INTEGRA1:def 8;
then A52: 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 A50, VALUED_1:13
.= ((upper_bound (rng (h | (divset D,j)))) - (lower_bound (rng (h | (divset D,j))))) * (vol (divset D,j)) ;
A53: (upper_bound (rng (h | (divset D,j)))) - (lower_bound (rng (h | (divset D,j)))) >= 0

proof

( rng (h | (divset D,j)) is bounded & ex r being Real st r in rng (h | (divset D,j)) )

proof

consider r being Real such that
A54: r in divset D,j by SUBSET_1:10;
j in dom D by A51, FINSEQ_1:def 3;
then divset D,j c= A by INTEGRA1:10;
then r in A by A54;
then r in dom h by FUNCT_2:def 1;
then r in (dom h) /\ (divset D,j) by A54, XBOOLE_0:def 4;
then r in dom (h | (divset D,j)) by RELAT_1:90;
then A55: (h | (divset D,j)) . r in rng (h | (divset D,j)) by FUNCT_1:def 5;
( h | A is bounded_above & h | A is bounded_below ) by A5;
then ( rng h is bounded_above & rng h is bounded_below ) by INTEGRA1:13, INTEGRA1:15;
then rng h is bounded ;
hence rng (h | (divset D,j)) is bounded by RELAT_1:99, XXREAL_2:45; :: thesis: ex r being Real st r in rng (h | (divset D,j))
thus ex r being Real st r in rng (h | (divset D,j)) by A55; :: thesis: verum

end;

hence (upper_bound (rng (h | (divset D,j)))) - (lower_bound (rng (h | (divset D,j)))) >= 0 by SEQ_4:24, XREAL_1:50; :: thesis: verum

end;

vol (divset D,j) >= 0 by INTEGRA1:11;
hence 0 <= F . j by A52, A53; :: thesis: verum

end;

hence osc2 . m >= 0 by A30, RVSUM_1:114; :: thesis: verum

end;

then A56: abs (osc2 . m) = osc2 . m by ABSVALUE:def 1;
reconsider G = UV1 - LV1 as FinSequence of REAL ;
reconsider H = UV - LV as FinSequence of REAL ;
A57: ( osc . m >= 0 & osc1 . m >= 0 )

proof

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 )
assume A58: j in dom H ; :: thesis: 0 <= H . j
set r = H . j;
j in Seg (len H) by A58, FINSEQ_1:def 3;
then A59: j in Seg (len D) by FINSEQ_1:def 18;
then j in dom D by FINSEQ_1:def 3;
then ( UV . j = (upper_bound (rng (f | (divset D,j)))) * (vol (divset D,j)) & LV . j = (lower_bound (rng (f | (divset D,j)))) * (vol (divset D,j)) ) by INTEGRA1:def 7, INTEGRA1:def 8;
then A60: 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 A58, VALUED_1:13
.= ((upper_bound (rng (f | (divset D,j)))) - (lower_bound (rng (f | (divset D,j))))) * (vol (divset D,j)) ;
A61: (upper_bound (rng (f | (divset D,j)))) - (lower_bound (rng (f | (divset D,j)))) >= 0

proof

( rng (f | (divset D,j)) is bounded & ex r being Real st r in rng (f | (divset D,j)) )

proof

consider r being Real such that
A62: r in divset D,j by SUBSET_1:10;
j in dom D by A59, FINSEQ_1:def 3;
then divset D,j c= A by INTEGRA1:10;
then r in A by A62;
then r in dom f by FUNCT_2:def 1;
then r in (dom f) /\ (divset D,j) by A62, XBOOLE_0:def 4;
then r in dom (f | (divset D,j)) by RELAT_1:90;
then A63: (f | (divset D,j)) . r in rng (f | (divset D,j)) by FUNCT_1:def 5;
( f | A is bounded_above & f | A is bounded_below ) by A1;
then ( rng f is bounded_above & rng f is bounded_below ) by INTEGRA1:13, INTEGRA1:15;
then rng f is bounded ;
hence rng (f | (divset D,j)) is bounded by RELAT_1:99, XXREAL_2:45; :: thesis: ex r being Real st r in rng (f | (divset D,j))
thus ex r being Real st r in rng (f | (divset D,j)) by A63; :: thesis: verum

end;

hence (upper_bound (rng (f | (divset D,j)))) - (lower_bound (rng (f | (divset D,j)))) >= 0 by SEQ_4:24, XREAL_1:50; :: thesis: verum

end;

vol (divset D,j) >= 0 by INTEGRA1:11;
hence 0 <= H . j by A60, A61; :: thesis: verum

end;

hence osc . m >= 0 by A27, RVSUM_1:114; :: thesis: osc1 . m >= 0
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 )
assume A64: j in dom G ; :: thesis: 0 <= G . j
set r = G . j;
j in Seg (len G) by A64, FINSEQ_1:def 3;
then A65: j in Seg (len D) by FINSEQ_1:def 18;
then j in dom D by FINSEQ_1:def 3;
then ( UV1 . j = (upper_bound (rng (g | (divset D,j)))) * (vol (divset D,j)) & LV1 . j = (lower_bound (rng (g | (divset D,j)))) * (vol (divset D,j)) ) by INTEGRA1:def 7, INTEGRA1:def 8;
then A66: 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 A64, VALUED_1:13
.= ((upper_bound (rng (g | (divset D,j)))) - (lower_bound (rng (g | (divset D,j))))) * (vol (divset D,j)) ;
A67: (upper_bound (rng (g | (divset D,j)))) - (lower_bound (rng (g | (divset D,j)))) >= 0

proof

( rng (g | (divset D,j)) is bounded & ex r being Real st r in rng (g | (divset D,j)) )

proof

consider r being Real such that
A68: r in divset D,j by SUBSET_1:10;
j in dom D by A65, FINSEQ_1:def 3;
then divset D,j c= A by INTEGRA1:10;
then r in A by A68;
then r in dom g by FUNCT_2:def 1;
then r in (dom g) /\ (divset D,j) by A68, XBOOLE_0:def 4;
then r in dom (g | (divset D,j)) by RELAT_1:90;
then A69: (g | (divset D,j)) . r in rng (g | (divset D,j)) by FUNCT_1:def 5;
( g | A is bounded_above & g | A is bounded_below ) by A3;
then ( rng g is bounded_above & rng g is bounded_below ) by INTEGRA1:13, INTEGRA1:15;
then rng g is bounded ;
hence rng (g | (divset D,j)) is bounded by RELAT_1:99, XXREAL_2:45; :: thesis: ex r being Real st r in rng (g | (divset D,j))
thus ex r being Real st r in rng (g | (divset D,j)) by A69; :: thesis: verum

end;

hence (upper_bound (rng (g | (divset D,j)))) - (lower_bound (rng (g | (divset D,j)))) >= 0 by SEQ_4:24, XREAL_1:50; :: thesis: verum

end;

vol (divset D,j) >= 0 by INTEGRA1:11;
hence 0 <= G . j by A66, A67; :: thesis: verum

end;

hence osc1 . m >= 0 by A28, RVSUM_1:114; :: thesis: verum

end;

then (osc . m) * (osc1 . m) >= 0 ;
then A70: (abs (osc . m)) + (abs (osc1 . m)) = abs ((osc . m) + (osc1 . m)) by ABSVALUE:24;
(osc . m) + (osc1 . m) >= 0 + 0 by A57;
then (abs ((osc . m) - 0 )) + (abs (osc1 . m)) = (osc . m) + (osc1 . m) by A70, ABSVALUE:def 1;
then (osc . m) + (osc1 . m) < ((b / a) / 2) + ((b / a) / 2) by A24, XREAL_1:10;
then a * ((osc . m) + (osc1 . m)) < a * (b / a) by A6, XREAL_1:70;
then a * ((osc . m) + (osc1 . m)) < b by A6, XCMPLX_1:88;
hence abs ((osc2 . m) - 0 ) < b by A49, A56, 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 lim ((upper_sum h,T) - (lower_sum h,T)) = 0 by A19, SEQ_2:def 7;
hence (lim (upper_sum h,T)) - (lim (lower_sum h,T)) = 0 by A12, SEQ_2:26; :: thesis: verum

end;

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