let A be non empty closed_interval Subset of REAL; :: thesis: for f being PartFunc of REAL,REAL st A c= dom f & f | A is continuous holds

f is_integrable_on A

let f be PartFunc of REAL,REAL; :: thesis: ( A c= dom f & f | A is continuous implies f is_integrable_on A )

assume A1: A c= dom f ; :: thesis: ( not f | A is continuous or f is_integrable_on A )

reconsider g = f | A as PartFunc of A,REAL by PARTFUN1:10;

A2: dom g = (dom f) /\ A by RELAT_1:61

.= A by A1, XBOOLE_1:28 ;

then A3: g is total by PARTFUN1:def 2;

for y being object st y in f .: A holds

y in rng g

for y being object st y in rng g holds

y in f .: A

then A9: rng g = f .: A by A6, XBOOLE_0:def 10;

assume A10: f | A is continuous ; :: thesis: f is_integrable_on A

then f .: A is real-bounded by A1, FCONT_1:29, RCOMP_1:10;

then A11: ( g | A is bounded_above & g | A is bounded_below ) by A9, INTEGRA1:12, INTEGRA1:14;

reconsider g = g as Function of A,REAL by A3;

A12: f | A is uniformly_continuous by A1, A10, FCONT_2:11;

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

hence f is_integrable_on A ; :: thesis: verum

f is_integrable_on A

let f be PartFunc of REAL,REAL; :: thesis: ( A c= dom f & f | A is continuous implies f is_integrable_on A )

assume A1: A c= dom f ; :: thesis: ( not f | A is continuous or f is_integrable_on A )

reconsider g = f | A as PartFunc of A,REAL by PARTFUN1:10;

A2: dom g = (dom f) /\ A by RELAT_1:61

.= A by A1, XBOOLE_1:28 ;

then A3: g is total by PARTFUN1:def 2;

for y being object st y in f .: A holds

y in rng g

proof

then A6:
f .: A c= rng g
by TARSKI:def 3;
let y be object ; :: thesis: ( y in f .: A implies y in rng g )

assume y in f .: A ; :: thesis: y in rng g

then consider x being object such that

x in dom f and

A4: x in A and

A5: y = f . x by FUNCT_1:def 6;

g . x in rng g by A2, A4, FUNCT_1:def 3;

hence y in rng g by A2, A4, A5, FUNCT_1:47; :: thesis: verum

end;assume y in f .: A ; :: thesis: y in rng g

then consider x being object such that

x in dom f and

A4: x in A and

A5: y = f . x by FUNCT_1:def 6;

g . x in rng g by A2, A4, FUNCT_1:def 3;

hence y in rng g by A2, A4, A5, FUNCT_1:47; :: thesis: verum

for y being object st y in rng g holds

y in f .: A

proof

then
rng g c= f .: A
by TARSKI:def 3;
let y be object ; :: thesis: ( y in rng g implies y in f .: A )

assume y in rng g ; :: thesis: y in f .: A

then consider x being object such that

A7: x in dom g and

A8: y = g . x by FUNCT_1:def 3;

f . x in f .: A by A1, A2, A7, FUNCT_1:def 6;

hence y in f .: A by A7, A8, FUNCT_1:47; :: thesis: verum

end;assume y in rng g ; :: thesis: y in f .: A

then consider x being object such that

A7: x in dom g and

A8: y = g . x by FUNCT_1:def 3;

f . x in f .: A by A1, A2, A7, FUNCT_1:def 6;

hence y in f .: A by A7, A8, FUNCT_1:47; :: thesis: verum

then A9: rng g = f .: A by A6, XBOOLE_0:def 10;

assume A10: f | A is continuous ; :: thesis: f is_integrable_on A

then f .: A is real-bounded by A1, FCONT_1:29, RCOMP_1:10;

then A11: ( g | A is bounded_above & g | A is bounded_below ) by A9, INTEGRA1:12, INTEGRA1:14;

reconsider g = g as Function of A,REAL by A3;

A12: f | A is uniformly_continuous by A1, A10, FCONT_2:11;

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

then
g is integrable
by A11, INTEGRA4:12;
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 )

reconsider osc = (upper_sum (g,T)) - (lower_sum (g,T)) as Real_Sequence ;

assume A13: ( delta T is convergent & lim (delta T) = 0 ) ; :: thesis: (lim (upper_sum (g,T))) - (lim (lower_sum (g,T))) = 0

A14: for r being Real st 0 < r holds

ex n being Nat st

for m being Nat st n <= m holds

|.((osc . m) - 0).| < r

then A50: lim osc = 0 by A14, SEQ_2:def 7;

( upper_sum (g,T) is convergent & lower_sum (g,T) is convergent ) by A11, A13, INTEGRA4:8, INTEGRA4:9;

hence (lim (upper_sum (g,T))) - (lim (lower_sum (g,T))) = 0 by A50, SEQ_2:12; :: thesis: verum

end;reconsider osc = (upper_sum (g,T)) - (lower_sum (g,T)) as Real_Sequence ;

assume A13: ( delta T is convergent & lim (delta T) = 0 ) ; :: thesis: (lim (upper_sum (g,T))) - (lim (lower_sum (g,T))) = 0

A14: for r being Real st 0 < r holds

ex n being Nat st

for m being Nat st n <= m holds

|.((osc . m) - 0).| < r

proof

then
osc is convergent
by SEQ_2:def 6;
let r be Real; :: thesis: ( 0 < r implies ex n being Nat st

for m being Nat st n <= m holds

|.((osc . m) - 0).| < r )

assume A15: r > 0 ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

|.((osc . m) - 0).| < r

ex r1 being Real st

( r1 > 0 & r1 * (vol A) < r )

A20: r1 > 0 and

A21: r1 * (vol A) < r ;

consider s being Real such that

A22: 0 < s and

A23: for x1, x2 being Real st x1 in dom (f | A) & x2 in dom (f | A) & |.(x1 - x2).| < s holds

|.((f . x1) - (f . x2)).| < r1 by A12, A20, FCONT_2:1;

consider n being Nat such that

A24: for m being Nat st n <= m holds

|.(((delta T) . m) - 0).| < s by A13, A22, SEQ_2:def 7;

A25: for m being Element of NAT st n <= m holds

((upper_sum (g,T)) . m) - ((lower_sum (g,T)) . m) <= r1 * (vol A)

|.((osc . m) - 0).| < r

let m be Nat; :: thesis: ( n <= m implies |.((osc . m) - 0).| < r )

reconsider mm = m as Element of NAT by ORDINAL1:def 12;

reconsider D = T . mm as Division of A ;

assume n <= m ; :: thesis: |.((osc . m) - 0).| < r

then ((upper_sum (g,T)) . mm) - ((lower_sum (g,T)) . mm) <= r1 * (vol A) by A25;

then A48: ((upper_sum (g,T)) . m) - ((lower_sum (g,T)) . m) < r by A21, XXREAL_0:2;

upper_sum (g,D) >= lower_sum (g,D) by A11, INTEGRA1:28;

then (upper_sum (g,T)) . mm >= lower_sum (g,D) by INTEGRA2:def 2;

then (upper_sum (g,T)) . mm >= (lower_sum (g,T)) . mm by INTEGRA2:def 3;

then A49: ((upper_sum (g,T)) . m) - ((lower_sum (g,T)) . m) >= 0 by XREAL_1:48;

osc . 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) ;

hence |.((osc . m) - 0).| < r by A48, A49, ABSVALUE:def 1; :: thesis: verum

end;for m being Nat st n <= m holds

|.((osc . m) - 0).| < r )

assume A15: r > 0 ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

|.((osc . m) - 0).| < r

ex r1 being Real st

( r1 > 0 & r1 * (vol A) < r )

proof
end;

then consider r1 being Real such that per cases
( vol A = 0 or vol A > 0 )
by INTEGRA1:9;

end;

suppose A16:
vol A = 0
; :: thesis: ex r1 being Real st

( r1 > 0 & r1 * (vol A) < r )

( r1 > 0 & r1 * (vol A) < r )

take
1
; :: thesis: ( 1 > 0 & 1 * (vol A) < r )

for r1 being Real holds r1 * (vol A) < r by A15, A16;

hence ( 1 > 0 & 1 * (vol A) < r ) ; :: thesis: verum

end;for r1 being Real holds r1 * (vol A) < r by A15, A16;

hence ( 1 > 0 & 1 * (vol A) < r ) ; :: thesis: verum

suppose A17:
vol A > 0
; :: thesis: ex r1 being Real st

( r1 > 0 & r1 * (vol A) < r )

( r1 > 0 & r1 * (vol A) < r )

then
r / (vol A) > 0
by A15, XREAL_1:139;

then consider r1 being Real such that

A18: 0 < r1 and

A19: r1 < r / (vol A) by XREAL_1:5;

take r1 ; :: thesis: ( r1 > 0 & r1 * (vol A) < r )

r1 * (vol A) < r by A17, A19, XREAL_1:79;

hence ( r1 > 0 & r1 * (vol A) < r ) by A18; :: thesis: verum

end;then consider r1 being Real such that

A18: 0 < r1 and

A19: r1 < r / (vol A) by XREAL_1:5;

take r1 ; :: thesis: ( r1 > 0 & r1 * (vol A) < r )

r1 * (vol A) < r by A17, A19, XREAL_1:79;

hence ( r1 > 0 & r1 * (vol A) < r ) by A18; :: thesis: verum

A20: r1 > 0 and

A21: r1 * (vol A) < r ;

consider s being Real such that

A22: 0 < s and

A23: for x1, x2 being Real st x1 in dom (f | A) & x2 in dom (f | A) & |.(x1 - x2).| < s holds

|.((f . x1) - (f . x2)).| < r1 by A12, A20, FCONT_2:1;

consider n being Nat such that

A24: for m being Nat st n <= m holds

|.(((delta T) . m) - 0).| < s by A13, A22, SEQ_2:def 7;

A25: for m being Element of NAT st n <= m holds

((upper_sum (g,T)) . m) - ((lower_sum (g,T)) . m) <= r1 * (vol A)

proof

take
n
; :: thesis: for m being Nat st n <= m holds
let m be Element of NAT ; :: thesis: ( n <= m implies ((upper_sum (g,T)) . m) - ((lower_sum (g,T)) . m) <= r1 * (vol A) )

reconsider D = T . m as Division of A ;

len (upper_volume (g,D)) = len D by INTEGRA1:def 6;

then reconsider UV = upper_volume (g,D) as Element of (len D) -tuples_on REAL by FINSEQ_2:92;

len (lower_volume (g,D)) = len D by INTEGRA1:def 7;

then reconsider LV = lower_volume (g,D) as Element of (len D) -tuples_on REAL by FINSEQ_2:92;

reconsider OSC = UV - LV as Element of (len D) -tuples_on REAL ;

len (upper_volume ((chi (A,A)),D)) = len D by INTEGRA1:def 6;

then reconsider VOL = upper_volume ((chi (A,A)),D) as Element of (len D) -tuples_on REAL by FINSEQ_2:92;

assume A26: n <= m ; :: thesis: ((upper_sum (g,T)) . m) - ((lower_sum (g,T)) . m) <= r1 * (vol A)

A27: for k being Element of NAT st k in dom D holds

((upper_volume (g,D)) . k) - ((lower_volume (g,D)) . k) <= r1 * ((upper_volume ((chi (A,A)),D)) . k)

OSC . k <= (r1 * VOL) . k

then Sum OSC <= r1 * (Sum VOL) by RVSUM_1:87;

then (Sum UV) - (Sum LV) <= r1 * (Sum VOL) by RVSUM_1:90;

then (upper_sum (g,D)) - (Sum LV) <= r1 * (Sum VOL) by INTEGRA1:def 8;

then (upper_sum (g,D)) - (lower_sum (g,D)) <= r1 * (Sum VOL) by INTEGRA1:def 9;

then (upper_sum (g,D)) - (lower_sum (g,D)) <= r1 * (vol A) by INTEGRA1:24;

then ((upper_sum (g,T)) . m) - (lower_sum (g,D)) <= r1 * (vol A) by INTEGRA2:def 2;

hence ((upper_sum (g,T)) . m) - ((lower_sum (g,T)) . m) <= r1 * (vol A) by INTEGRA2:def 3; :: thesis: verum

end;reconsider D = T . m as Division of A ;

len (upper_volume (g,D)) = len D by INTEGRA1:def 6;

then reconsider UV = upper_volume (g,D) as Element of (len D) -tuples_on REAL by FINSEQ_2:92;

len (lower_volume (g,D)) = len D by INTEGRA1:def 7;

then reconsider LV = lower_volume (g,D) as Element of (len D) -tuples_on REAL by FINSEQ_2:92;

reconsider OSC = UV - LV as Element of (len D) -tuples_on REAL ;

len (upper_volume ((chi (A,A)),D)) = len D by INTEGRA1:def 6;

then reconsider VOL = upper_volume ((chi (A,A)),D) as Element of (len D) -tuples_on REAL by FINSEQ_2:92;

assume A26: n <= m ; :: thesis: ((upper_sum (g,T)) . m) - ((lower_sum (g,T)) . m) <= r1 * (vol A)

A27: for k being Element of NAT st k in dom D holds

((upper_volume (g,D)) . k) - ((lower_volume (g,D)) . k) <= r1 * ((upper_volume ((chi (A,A)),D)) . k)

proof

for k being Nat st k in Seg (len D) holds
let k be Element of NAT ; :: thesis: ( k in dom D implies ((upper_volume (g,D)) . k) - ((lower_volume (g,D)) . k) <= r1 * ((upper_volume ((chi (A,A)),D)) . k) )

assume A28: k in dom D ; :: thesis: ((upper_volume (g,D)) . k) - ((lower_volume (g,D)) . k) <= r1 * ((upper_volume ((chi (A,A)),D)) . k)

reconsider h = g | (divset (D,k)) as PartFunc of (divset (D,k)),REAL by PARTFUN1:10;

dom g = A by PARTFUN1:def 2;

then (dom g) /\ (divset (D,k)) = divset (D,k) by A28, INTEGRA1:8, XBOOLE_1:28;

then dom h = divset (D,k) by RELAT_1:61;

then h is total by PARTFUN1:def 2;

then reconsider h = h as Function of (divset (D,k)),REAL ;

A29: for x1, x2 being Real st x1 in divset (D,k) & x2 in divset (D,k) holds

|.((h . x1) - (h . x2)).| <= r1

then ((upper_bound (rng (g | (divset (D,k))))) - (lower_bound (rng (g | (divset (D,k)))))) * (vol (divset (D,k))) <= r1 * (vol (divset (D,k))) by A29, INTEGRA4:24, XREAL_1:64;

then ((upper_bound (rng (g | (divset (D,k))))) * (vol (divset (D,k)))) - ((lower_bound (rng (g | (divset (D,k))))) * (vol (divset (D,k)))) <= r1 * (vol (divset (D,k))) ;

then ((upper_volume (g,D)) . k) - ((lower_bound (rng (g | (divset (D,k))))) * (vol (divset (D,k)))) <= r1 * (vol (divset (D,k))) by A28, INTEGRA1:def 6;

then ((upper_volume (g,D)) . k) - ((lower_volume (g,D)) . k) <= r1 * (vol (divset (D,k))) by A28, INTEGRA1:def 7;

hence ((upper_volume (g,D)) . k) - ((lower_volume (g,D)) . k) <= r1 * ((upper_volume ((chi (A,A)),D)) . k) by A28, INTEGRA1:20; :: thesis: verum

end;assume A28: k in dom D ; :: thesis: ((upper_volume (g,D)) . k) - ((lower_volume (g,D)) . k) <= r1 * ((upper_volume ((chi (A,A)),D)) . k)

reconsider h = g | (divset (D,k)) as PartFunc of (divset (D,k)),REAL by PARTFUN1:10;

dom g = A by PARTFUN1:def 2;

then (dom g) /\ (divset (D,k)) = divset (D,k) by A28, INTEGRA1:8, XBOOLE_1:28;

then dom h = divset (D,k) by RELAT_1:61;

then h is total by PARTFUN1:def 2;

then reconsider h = h as Function of (divset (D,k)),REAL ;

A29: for x1, x2 being Real st x1 in divset (D,k) & x2 in divset (D,k) holds

|.((h . x1) - (h . x2)).| <= r1

proof

vol (divset (D,k)) >= 0
by INTEGRA1:9;
(upper_volume ((chi (A,A)),D)) . k = vol (divset (D,k))
by A28, INTEGRA1:20;

then A30: (upper_volume ((chi (A,A)),D)) . k >= 0 by INTEGRA1:9;

k in Seg (len D) by A28, FINSEQ_1:def 3;

then k in Seg (len (upper_volume ((chi (A,A)),D))) by INTEGRA1:def 6;

then k in dom (upper_volume ((chi (A,A)),D)) by FINSEQ_1:def 3;

then A31: (upper_volume ((chi (A,A)),D)) . k in rng (upper_volume ((chi (A,A)),D)) by FUNCT_1:def 3;

dom h = (dom g) /\ (divset (D,k)) by RELAT_1:61;

then A32: dom h c= dom g by XBOOLE_1:17;

let x1, x2 be Real; :: thesis: ( x1 in divset (D,k) & x2 in divset (D,k) implies |.((h . x1) - (h . x2)).| <= r1 )

assume that

A33: x1 in divset (D,k) and

A34: x2 in divset (D,k) ; :: thesis: |.((h . x1) - (h . x2)).| <= r1

A35: x2 in dom h by A34, PARTFUN1:def 2;

then g . x2 = h . x2 by FUNCT_1:47;

then A36: f . x2 = h . x2 by A35, A32, FUNCT_1:47;

A37: |.(x1 - x2).| <= (delta T) . m

.= max (rng (upper_volume ((chi (A,A)),D))) by INTEGRA3:def 1 ;

then ((delta T) . m) - 0 >= 0 by A30, A31, XXREAL_2:def 8;

then A44: |.(x1 - x2).| <= |.(((delta T) . m) - 0).| by A37, ABSVALUE:def 1;

|.(((delta T) . m) - 0).| < s by A24, A26;

then A45: |.(x1 - x2).| < s by A44, XXREAL_0:2;

A46: x1 in dom h by A33, PARTFUN1:def 2;

then g . x1 = h . x1 by FUNCT_1:47;

then f . x1 = h . x1 by A46, A32, FUNCT_1:47;

hence |.((h . x1) - (h . x2)).| <= r1 by A23, A45, A46, A35, A32, A36; :: thesis: verum

end;then A30: (upper_volume ((chi (A,A)),D)) . k >= 0 by INTEGRA1:9;

k in Seg (len D) by A28, FINSEQ_1:def 3;

then k in Seg (len (upper_volume ((chi (A,A)),D))) by INTEGRA1:def 6;

then k in dom (upper_volume ((chi (A,A)),D)) by FINSEQ_1:def 3;

then A31: (upper_volume ((chi (A,A)),D)) . k in rng (upper_volume ((chi (A,A)),D)) by FUNCT_1:def 3;

dom h = (dom g) /\ (divset (D,k)) by RELAT_1:61;

then A32: dom h c= dom g by XBOOLE_1:17;

let x1, x2 be Real; :: thesis: ( x1 in divset (D,k) & x2 in divset (D,k) implies |.((h . x1) - (h . x2)).| <= r1 )

assume that

A33: x1 in divset (D,k) and

A34: x2 in divset (D,k) ; :: thesis: |.((h . x1) - (h . x2)).| <= r1

A35: x2 in dom h by A34, PARTFUN1:def 2;

then g . x2 = h . x2 by FUNCT_1:47;

then A36: f . x2 = h . x2 by A35, A32, FUNCT_1:47;

A37: |.(x1 - x2).| <= (delta T) . m

proof

end;

(delta T) . m =
delta D
by INTEGRA3:def 2
now :: thesis: |.(x1 - x2).| <= (delta T) . mend;

hence
|.(x1 - x2).| <= (delta T) . m
; :: thesis: verumper cases
( x1 >= x2 or x1 < x2 )
;

end;

suppose
x1 >= x2
; :: thesis: |.(x1 - x2).| <= (delta T) . m

then
x1 - x2 >= 0
by XREAL_1:48;

then A38: |.(x1 - x2).| = x1 - x2 by ABSVALUE:def 1;

( x1 <= upper_bound (divset (D,k)) & x2 >= lower_bound (divset (D,k)) ) by A33, A34, INTEGRA2:1;

then |.(x1 - x2).| <= (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) by A38, XREAL_1:13;

then A39: |.(x1 - x2).| <= vol (divset (D,k)) by INTEGRA1:def 5;

k in Seg (len D) by A28, FINSEQ_1:def 3;

then k in Seg (len (upper_volume ((chi (A,A)),D))) by INTEGRA1:def 6;

then k in dom (upper_volume ((chi (A,A)),D)) by FINSEQ_1:def 3;

then (upper_volume ((chi (A,A)),D)) . k in rng (upper_volume ((chi (A,A)),D)) by FUNCT_1:def 3;

then (upper_volume ((chi (A,A)),D)) . k <= max (rng (upper_volume ((chi (A,A)),D))) by XXREAL_2:def 8;

then A40: (upper_volume ((chi (A,A)),D)) . k <= delta (T . m) by INTEGRA3:def 1;

(upper_volume ((chi (A,A)),D)) . k = vol (divset (D,k)) by A28, INTEGRA1:20;

then |.(x1 - x2).| <= delta (T . m) by A39, A40, XXREAL_0:2;

hence |.(x1 - x2).| <= (delta T) . m by INTEGRA3:def 2; :: thesis: verum

end;then A38: |.(x1 - x2).| = x1 - x2 by ABSVALUE:def 1;

( x1 <= upper_bound (divset (D,k)) & x2 >= lower_bound (divset (D,k)) ) by A33, A34, INTEGRA2:1;

then |.(x1 - x2).| <= (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) by A38, XREAL_1:13;

then A39: |.(x1 - x2).| <= vol (divset (D,k)) by INTEGRA1:def 5;

k in Seg (len D) by A28, FINSEQ_1:def 3;

then k in Seg (len (upper_volume ((chi (A,A)),D))) by INTEGRA1:def 6;

then k in dom (upper_volume ((chi (A,A)),D)) by FINSEQ_1:def 3;

then (upper_volume ((chi (A,A)),D)) . k in rng (upper_volume ((chi (A,A)),D)) by FUNCT_1:def 3;

then (upper_volume ((chi (A,A)),D)) . k <= max (rng (upper_volume ((chi (A,A)),D))) by XXREAL_2:def 8;

then A40: (upper_volume ((chi (A,A)),D)) . k <= delta (T . m) by INTEGRA3:def 1;

(upper_volume ((chi (A,A)),D)) . k = vol (divset (D,k)) by A28, INTEGRA1:20;

then |.(x1 - x2).| <= delta (T . m) by A39, A40, XXREAL_0:2;

hence |.(x1 - x2).| <= (delta T) . m by INTEGRA3:def 2; :: thesis: verum

suppose
x1 < x2
; :: thesis: |.(x1 - x2).| <= (delta T) . m

then
x1 - x2 < 0
by XREAL_1:49;

then |.(x1 - x2).| = - (x1 - x2) by ABSVALUE:def 1;

then A41: |.(x1 - x2).| = x2 - x1 ;

( x2 <= upper_bound (divset (D,k)) & x1 >= lower_bound (divset (D,k)) ) by A33, A34, INTEGRA2:1;

then |.(x1 - x2).| <= (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) by A41, XREAL_1:13;

then A42: |.(x1 - x2).| <= vol (divset (D,k)) by INTEGRA1:def 5;

k in Seg (len D) by A28, FINSEQ_1:def 3;

then k in Seg (len (upper_volume ((chi (A,A)),D))) by INTEGRA1:def 6;

then k in dom (upper_volume ((chi (A,A)),D)) by FINSEQ_1:def 3;

then (upper_volume ((chi (A,A)),D)) . k in rng (upper_volume ((chi (A,A)),D)) by FUNCT_1:def 3;

then (upper_volume ((chi (A,A)),D)) . k <= max (rng (upper_volume ((chi (A,A)),D))) by XXREAL_2:def 8;

then A43: (upper_volume ((chi (A,A)),D)) . k <= delta (T . m) by INTEGRA3:def 1;

(upper_volume ((chi (A,A)),D)) . k = vol (divset (D,k)) by A28, INTEGRA1:20;

then |.(x1 - x2).| <= delta (T . m) by A42, A43, XXREAL_0:2;

hence |.(x1 - x2).| <= (delta T) . m by INTEGRA3:def 2; :: thesis: verum

end;then |.(x1 - x2).| = - (x1 - x2) by ABSVALUE:def 1;

then A41: |.(x1 - x2).| = x2 - x1 ;

( x2 <= upper_bound (divset (D,k)) & x1 >= lower_bound (divset (D,k)) ) by A33, A34, INTEGRA2:1;

then |.(x1 - x2).| <= (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) by A41, XREAL_1:13;

then A42: |.(x1 - x2).| <= vol (divset (D,k)) by INTEGRA1:def 5;

k in Seg (len D) by A28, FINSEQ_1:def 3;

then k in Seg (len (upper_volume ((chi (A,A)),D))) by INTEGRA1:def 6;

then k in dom (upper_volume ((chi (A,A)),D)) by FINSEQ_1:def 3;

then (upper_volume ((chi (A,A)),D)) . k in rng (upper_volume ((chi (A,A)),D)) by FUNCT_1:def 3;

then (upper_volume ((chi (A,A)),D)) . k <= max (rng (upper_volume ((chi (A,A)),D))) by XXREAL_2:def 8;

then A43: (upper_volume ((chi (A,A)),D)) . k <= delta (T . m) by INTEGRA3:def 1;

(upper_volume ((chi (A,A)),D)) . k = vol (divset (D,k)) by A28, INTEGRA1:20;

then |.(x1 - x2).| <= delta (T . m) by A42, A43, XXREAL_0:2;

hence |.(x1 - x2).| <= (delta T) . m by INTEGRA3:def 2; :: thesis: verum

.= max (rng (upper_volume ((chi (A,A)),D))) by INTEGRA3:def 1 ;

then ((delta T) . m) - 0 >= 0 by A30, A31, XXREAL_2:def 8;

then A44: |.(x1 - x2).| <= |.(((delta T) . m) - 0).| by A37, ABSVALUE:def 1;

|.(((delta T) . m) - 0).| < s by A24, A26;

then A45: |.(x1 - x2).| < s by A44, XXREAL_0:2;

A46: x1 in dom h by A33, PARTFUN1:def 2;

then g . x1 = h . x1 by FUNCT_1:47;

then f . x1 = h . x1 by A46, A32, FUNCT_1:47;

hence |.((h . x1) - (h . x2)).| <= r1 by A23, A45, A46, A35, A32, A36; :: thesis: verum

then ((upper_bound (rng (g | (divset (D,k))))) - (lower_bound (rng (g | (divset (D,k)))))) * (vol (divset (D,k))) <= r1 * (vol (divset (D,k))) by A29, INTEGRA4:24, XREAL_1:64;

then ((upper_bound (rng (g | (divset (D,k))))) * (vol (divset (D,k)))) - ((lower_bound (rng (g | (divset (D,k))))) * (vol (divset (D,k)))) <= r1 * (vol (divset (D,k))) ;

then ((upper_volume (g,D)) . k) - ((lower_bound (rng (g | (divset (D,k))))) * (vol (divset (D,k)))) <= r1 * (vol (divset (D,k))) by A28, INTEGRA1:def 6;

then ((upper_volume (g,D)) . k) - ((lower_volume (g,D)) . k) <= r1 * (vol (divset (D,k))) by A28, INTEGRA1:def 7;

hence ((upper_volume (g,D)) . k) - ((lower_volume (g,D)) . k) <= r1 * ((upper_volume ((chi (A,A)),D)) . k) by A28, INTEGRA1:20; :: thesis: verum

OSC . k <= (r1 * VOL) . k

proof

then
Sum OSC <= Sum (r1 * VOL)
by RVSUM_1:82;
let k be Nat; :: thesis: ( k in Seg (len D) implies OSC . k <= (r1 * VOL) . k )

assume k in Seg (len D) ; :: thesis: OSC . k <= (r1 * VOL) . k

then A47: k in dom D by FINSEQ_1:def 3;

OSC . k = ((upper_volume (g,D)) . k) - ((lower_volume (g,D)) . k) by RVSUM_1:27;

then OSC . k <= r1 * (VOL . k) by A27, A47;

hence OSC . k <= (r1 * VOL) . k by RVSUM_1:45; :: thesis: verum

end;assume k in Seg (len D) ; :: thesis: OSC . k <= (r1 * VOL) . k

then A47: k in dom D by FINSEQ_1:def 3;

OSC . k = ((upper_volume (g,D)) . k) - ((lower_volume (g,D)) . k) by RVSUM_1:27;

then OSC . k <= r1 * (VOL . k) by A27, A47;

hence OSC . k <= (r1 * VOL) . k by RVSUM_1:45; :: thesis: verum

then Sum OSC <= r1 * (Sum VOL) by RVSUM_1:87;

then (Sum UV) - (Sum LV) <= r1 * (Sum VOL) by RVSUM_1:90;

then (upper_sum (g,D)) - (Sum LV) <= r1 * (Sum VOL) by INTEGRA1:def 8;

then (upper_sum (g,D)) - (lower_sum (g,D)) <= r1 * (Sum VOL) by INTEGRA1:def 9;

then (upper_sum (g,D)) - (lower_sum (g,D)) <= r1 * (vol A) by INTEGRA1:24;

then ((upper_sum (g,T)) . m) - (lower_sum (g,D)) <= r1 * (vol A) by INTEGRA2:def 2;

hence ((upper_sum (g,T)) . m) - ((lower_sum (g,T)) . m) <= r1 * (vol A) by INTEGRA2:def 3; :: thesis: verum

|.((osc . m) - 0).| < r

let m be Nat; :: thesis: ( n <= m implies |.((osc . m) - 0).| < r )

reconsider mm = m as Element of NAT by ORDINAL1:def 12;

reconsider D = T . mm as Division of A ;

assume n <= m ; :: thesis: |.((osc . m) - 0).| < r

then ((upper_sum (g,T)) . mm) - ((lower_sum (g,T)) . mm) <= r1 * (vol A) by A25;

then A48: ((upper_sum (g,T)) . m) - ((lower_sum (g,T)) . m) < r by A21, XXREAL_0:2;

upper_sum (g,D) >= lower_sum (g,D) by A11, INTEGRA1:28;

then (upper_sum (g,T)) . mm >= lower_sum (g,D) by INTEGRA2:def 2;

then (upper_sum (g,T)) . mm >= (lower_sum (g,T)) . mm by INTEGRA2:def 3;

then A49: ((upper_sum (g,T)) . m) - ((lower_sum (g,T)) . m) >= 0 by XREAL_1:48;

osc . 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) ;

hence |.((osc . m) - 0).| < r by A48, A49, ABSVALUE:def 1; :: thesis: verum

then A50: lim osc = 0 by A14, SEQ_2:def 7;

( upper_sum (g,T) is convergent & lower_sum (g,T) is convergent ) by A11, A13, INTEGRA4:8, INTEGRA4:9;

hence (lim (upper_sum (g,T))) - (lim (lower_sum (g,T))) = 0 by A50, SEQ_2:12; :: thesis: verum

hence f is_integrable_on A ; :: thesis: verum