let A be non empty closed_interval Subset of REAL; :: thesis:
let f be PartFunc of REAL,REAL; :: thesis:
assume A1: A c= dom f ; :: thesis:
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

let y be object ; :: thesis:
assume y in f .: A ; :: thesis:
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:

end;

then A6: f .: A c= rng g by TARSKI:def 3;
for y being object st y in rng g holds
y in f .: A

proof

let y be object ; :: thesis:
assume y in rng g ; :: thesis:
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:

end;

then rng g c= f .: A by TARSKI:def 3;
then A9: rng g = f .: A by A6, XBOOLE_0:def 10;
assume A10: f | A is continuous ; :: thesis:
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

let T be DivSequence of A; :: thesis:
reconsider osc = (upper_sum (g,T)) - (lower_sum (g,T)) as Real_Sequence ;
assume A13: ( delta T is convergent & lim (delta T) = 0 ) ; :: thesis:
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

let r be Real; :: thesis:
assume A15: r > 0 ; :: thesis:
ex r1 being Real st
( r1 > 0 & r1 * (vol A) < r )

proof

per cases by INTEGRA1:9;

suppose A16: vol A = 0 ; :: thesis:

take 1 ; :: thesis:
for r1 being Real holds r1 * (vol A) < r by A15, A16;
hence ( 1 > 0 & 1 * (vol A) < r ) ; :: thesis:

end;

suppose A17: vol A > 0 ; :: thesis:

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 * (vol A) < r by A17, A19, XREAL_1:79;
hence ( r1 > 0 & r1 * (vol A) < r ) by A18; :: thesis:

end;

then consider r1 being Real such that
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

let m be Element of NAT ; :: thesis:
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:
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

let k be Element of NAT ; :: thesis:
assume A28: k in dom D ; :: thesis:
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

(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:
assume that
A33: x1 in divset (D,k) and
A34: x2 in divset (D,k) ; :: thesis:
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

now :: thesis:

per cases ;

suppose x1 >= x2 ; :: thesis:

end;

suppose x1 < x2 ; :: thesis:

end;

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

end;

(delta T) . m = delta D by INTEGRA3:def 2
.= 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:

end;

end;

for k being Nat st k in Seg (len D) holds
OSC . k <= (r1 * VOL) . k

proof

let k be Nat; :: thesis:
assume k in Seg (len D) ; :: thesis:
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:

end;

then Sum OSC <= Sum (r1 * VOL) by RVSUM_1:82;
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:

end;

take n ; :: thesis:
let m be Nat; :: thesis:
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
reconsider D = T . mm as Division of A ;
assume n <= m ; :: thesis:
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:

end;

then osc is convergent by SEQ_2:def 6;
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:

end;

then g is integrable by A11, INTEGRA4:12;
hence f is_integrable_on A ; :: thesis: