let A be 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:43;
A2: dom g = (dom f) /\ A by RELAT_1:90
.= A by A1, XBOOLE_1:28 ;
then A3: g is total by PARTFUN1:def 4;
for y being set st y in f .: A holds
y in rng g

proof

let y be set ; :: thesis:
assume y in f .: A ; :: thesis:
then consider x being set such that
x in dom f and
A4: x in A and
A5: y = f . x by FUNCT_1:def 12;
g . x in rng g by A2, A4, FUNCT_1:def 5;
hence y in rng g by A2, A4, A5, FUNCT_1:70; :: thesis:

end;

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

proof

let y be set ; :: thesis:
assume y in rng g ; :: thesis:
then consider x being set such that
A7: x in dom g and
A8: y = g . x by FUNCT_1:def 5;
f . x in f .: A by A1, A2, A7, FUNCT_1:def 12;
hence y in f .: A by A7, A8, FUNCT_1:70; :: 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 bounded by A1, FCONT_1:30, RCOMP_1:28;
then A11: ( g | A is bounded_above & g | A is bounded_below ) by A9, INTEGRA1:14, INTEGRA1:16;
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 number st 0 < r holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((osc . m) - 0 ) < r

proof

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

proof

now

per cases by INTEGRA1:11;

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

consider r1 being Real such that
A17: r1 = 1 ;
r1 * (vol A) < r by A15, A16;
hence ex r1 being Real st
( r1 > 0 & r1 * (vol A) < r ) by A17; :: thesis:

end;

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

then r / (vol A) > 0 by A15, XREAL_1:141;
then consider r1 being real number such that
A19: 0 < r1 and
A20: r1 < r / (vol A) by XREAL_1:7;
reconsider r1 = r1 as Real by XREAL_0:def 1;
r1 * (vol A) < r by A18, A20, XREAL_1:81;
hence ex r1 being Real st
( r1 > 0 & r1 * (vol A) < r ) by A19; :: thesis:

end;

hence ex r1 being Real st
( r1 > 0 & r1 * (vol A) < r ) ; :: thesis:

end;

then consider r1 being Real such that
A21: r1 > 0 and
A22: r1 * (vol A) < r ;
consider s being Real such that
A23: 0 < s and
A24: for x1, x2 being Real st x1 in dom (f | A) & x2 in dom (f | A) & abs (x1 - x2) < s holds
abs ((f . x1) - (f . x2)) < r1 by A12, A21, FCONT_2:1;
consider n being Element of NAT such that
A25: for m being Element of NAT st n <= m holds
abs (((delta T) . m) - 0 ) < s by A13, A23, SEQ_2:def 7;
A26: 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 7;
then reconsider UV = upper_volume g,D as Element of (len D) -tuples_on REAL by FINSEQ_2:110;
len (lower_volume g,D) = len D by INTEGRA1:def 8;
then reconsider LV = lower_volume g,D as Element of (len D) -tuples_on REAL by FINSEQ_2:110;
reconsider OSC = UV - LV as Element of (len D) -tuples_on REAL ;
len (upper_volume (chi A,A),D) = len D by INTEGRA1:def 7;
then reconsider VOL = upper_volume (chi A,A),D as Element of (len D) -tuples_on REAL by FINSEQ_2:110;
assume A27: n <= m ; :: thesis:
A28: 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 A29: k in dom D ; :: thesis:
reconsider h = g | (divset D,k) as PartFunc of (divset D,k),REAL by PARTFUN1:43;
dom g = A by PARTFUN1:def 4;
then (dom g) /\ (divset D,k) = divset D,k by A29, INTEGRA1:10, XBOOLE_1:28;
then dom h = divset D,k by RELAT_1:90;
then h is total by PARTFUN1:def 4;
then reconsider h = h as Function of (divset D,k),REAL ;
A30: for x1, x2 being Real st x1 in divset D,k & x2 in divset D,k holds
abs ((h . x1) - (h . x2)) <= r1

proof

(upper_volume (chi A,A),D) . k = vol (divset D,k) by A29, INTEGRA1:22;
then A31: (upper_volume (chi A,A),D) . k >= 0 by INTEGRA1:11;
k in Seg (len D) by A29, FINSEQ_1:def 3;
then k in Seg (len (upper_volume (chi A,A),D)) by INTEGRA1:def 7;
then k in dom (upper_volume (chi A,A),D) by FINSEQ_1:def 3;
then A32: (upper_volume (chi A,A),D) . k in rng (upper_volume (chi A,A),D) by FUNCT_1:def 5;
dom h = (dom g) /\ (divset D,k) by RELAT_1:90;
then A33: dom h c= dom g by XBOOLE_1:17;
let x1, x2 be Real; :: thesis:
assume that
A34: x1 in divset D,k and
A35: x2 in divset D,k ; :: thesis:
A36: x2 in dom h by A35, PARTFUN1:def 4;
then g . x2 = h . x2 by FUNCT_1:70;
then A37: f . x2 = h . x2 by A36, A33, FUNCT_1:70;
A38: abs (x1 - x2) <= (delta T) . m

proof

now

per cases ;

suppose x1 >= x2 ; :: thesis:

end;

suppose x1 < x2 ; :: thesis:

end;

hence abs (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 A31, A32, XXREAL_2:def 8;
then A45: abs (x1 - x2) <= abs (((delta T) . m) - 0 ) by A38, ABSVALUE:def 1;
abs (((delta T) . m) - 0 ) < s by A25, A27;
then A46: abs (x1 - x2) < s by A45, XXREAL_0:2;
A47: x1 in dom h by A34, PARTFUN1:def 4;
then g . x1 = h . x1 by FUNCT_1:70;
then f . x1 = h . x1 by A47, A33, FUNCT_1:70;
hence abs ((h . x1) - (h . x2)) <= r1 by A24, A46, A47, A36, A33, A37; :: thesis:

end;

vol (divset D,k) >= 0 by INTEGRA1:11;
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 A30, INTEGRA4:24, XREAL_1:66;
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 A29, INTEGRA1:def 7;
then ((upper_volume g,D) . k) - ((lower_volume g,D) . k) <= r1 * (vol (divset D,k)) by A29, INTEGRA1:def 8;
hence ((upper_volume g,D) . k) - ((lower_volume g,D) . k) <= r1 * ((upper_volume (chi A,A),D) . k) by A29, INTEGRA1:22; :: thesis:

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 A48: k in dom D by FINSEQ_1:def 3;
OSC . k = ((upper_volume g,D) . k) - ((lower_volume g,D) . k) by RVSUM_1:48;
then OSC . k <= r1 * (VOL . k) by A28, A48;
hence OSC . k <= (r1 * VOL) . k by RVSUM_1:67; :: thesis:

end;

then Sum OSC <= Sum (r1 * VOL) by RVSUM_1:112;
then Sum OSC <= r1 * (Sum VOL) by RVSUM_1:117;
then (Sum UV) - (Sum LV) <= r1 * (Sum VOL) by RVSUM_1:120;
then (upper_sum g,D) - (Sum LV) <= r1 * (Sum VOL) by INTEGRA1:def 9;
then (upper_sum g,D) - (lower_sum g,D) <= r1 * (Sum VOL) by INTEGRA1:def 10;
then (upper_sum g,D) - (lower_sum g,D) <= r1 * (vol A) by INTEGRA1:26;
then ((upper_sum g,T) . m) - (lower_sum g,D) <= r1 * (vol A) by INTEGRA2:def 4;
hence ((upper_sum g,T) . m) - ((lower_sum g,T) . m) <= r1 * (vol A) by INTEGRA2:def 5; :: thesis:

end;

for m being Element of NAT st n <= m holds
abs ((osc . m) - 0 ) < r

proof

let m be Element of NAT ; :: thesis:
reconsider D = T . m as Division of A ;
assume n <= m ; :: thesis:
then ((upper_sum g,T) . m) - ((lower_sum g,T) . m) <= r1 * (vol A) by A26;
then A49: ((upper_sum g,T) . m) - ((lower_sum g,T) . m) < r by A22, XXREAL_0:2;
upper_sum g,D >= lower_sum g,D by A11, INTEGRA1:30;
then (upper_sum g,T) . m >= lower_sum g,D by INTEGRA2:def 4;
then (upper_sum g,T) . m >= (lower_sum g,T) . m by INTEGRA2:def 5;
then A50: ((upper_sum g,T) . m) - ((lower_sum g,T) . m) >= 0 by XREAL_1:50;
osc . 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) ;
hence abs ((osc . m) - 0 ) < r by A49, A50, ABSVALUE:def 1; :: thesis:

end;

hence ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((osc . m) - 0 ) < r ; :: thesis:

end;

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

end;

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