let A be 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 Z: A c= dom f ; :: thesis: ( not f | A is continuous or f is_integrable_on A )
assume A1: f | A is continuous ; :: thesis: f is_integrable_on A
then A2: f | A is uniformly_continuous by Z, FCONT_2:11;
reconsider g = f | A as PartFunc of A,REAL by PARTFUN1:43;
A4: ( g is total & g | A is bounded )

proof

A5: dom g = (dom f) /\ A by RELAT_1:90
.= A by Z, XBOOLE_1:28 ;
hence g is total by PARTFUN1:def 4; :: thesis: g | A is bounded
f .: A is compact by A1, Z, FCONT_1:30;
then A6: f .: A is bounded by RCOMP_1:28;
rng g = f .: A

proof

for y being set st y in rng g holds
y in f .: A

proof

let y be set ; :: thesis: ( y in rng g implies y in f .: A )
assume y in rng g ; :: thesis: y in f .: A
then consider x being set such that
A7: ( x in dom g & y = g . x ) by FUNCT_1:def 5;
f . x in f .: A by A5, A7, Z, FUNCT_1:def 12;
hence y in f .: A by A7, FUNCT_1:70; :: thesis: verum

end;

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

proof

let y be set ; :: thesis: ( y in f .: A implies y in rng g )
assume y in f .: A ; :: thesis: y in rng g
then consider x being set such that
A9: ( x in dom f & x in A & y = f . x ) by FUNCT_1:def 12;
( g . x in rng g & y = g . x ) by A5, A9, FUNCT_1:70, FUNCT_1:def 5;
hence y in rng g ; :: thesis: verum

end;

then f .: A c= rng g by TARSKI:def 3;
hence rng g = f .: A by A8, XBOOLE_0:def 10; :: thesis: verum

end;

then ( rng g is bounded_above & rng g is bounded_below ) by A6;
then ( g | A is bounded_above & g | A is bounded_below ) by INTEGRA1:14, INTEGRA1:16;
hence g | A is bounded ; :: thesis: verum

end;

then reconsider g = g as Function of A,REAL ;
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: ( delta T is convergent & lim (delta T) = 0 implies (lim (upper_sum g,T)) - (lim (lower_sum g,T)) = 0 )
assume that
A10: delta T is convergent and
A11: lim (delta T) = 0 ; :: thesis: (lim (upper_sum g,T)) - (lim (lower_sum g,T)) = 0
reconsider osc = (upper_sum g,T) - (lower_sum g,T) as Real_Sequence ;
A12: 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: ( 0 < r implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((osc . m) - 0 ) < r )
assume A13: r > 0 ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((osc . m) - 0 ) < r
ex r1 being Real st
( r1 > 0 & r1 * (vol A) < r )

proof

now

per cases ( vol A = 0 or vol A > 0 ) by INTEGRA1:11;

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

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

end;

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

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

end;

end;

end;

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

end;

then consider r1 being Real such that
A18: ( r1 > 0 & r1 * (vol A) < r ) ;
consider s being Real such that
A19: ( 0 < s & ( 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 A2, A18, FCONT_2:1;
consider n being Element of NAT such that
A20: for m being Element of NAT st n <= m holds
abs (((delta T) . m) - 0 ) < s by A10, A11, A19, SEQ_2:def 7;
A21: 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: ( n <= m implies ((upper_sum g,T) . m) - ((lower_sum g,T) . m) <= r1 * (vol A) )
assume A22: n <= m ; :: thesis: ((upper_sum g,T) . m) - ((lower_sum g,T) . m) <= r1 * (vol A)
reconsider D = T . m as Division of A ;
A23: 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: ( k in dom D implies ((upper_volume g,D) . k) - ((lower_volume g,D) . k) <= r1 * ((upper_volume (chi A,A),D) . k) )
assume A24: 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:43;
( h is total & h | (divset D,k) is bounded )

proof

dom g = A by PARTFUN1:def 4;
then (dom g) /\ (divset D,k) = divset D,k by A24, INTEGRA1:10, XBOOLE_1:28;
then dom h = divset D,k by RELAT_1:90;
hence h is total by PARTFUN1:def 4; :: thesis: h | (divset D,k) is bounded
( g | A is bounded_above & g | A is bounded_below ) by A4;
then ( rng h is bounded_above & rng h is bounded_below ) by INTEGRA4:18, INTEGRA4:19;
then ( h | (divset D,k) is bounded_above & h | (divset D,k) is bounded_below ) by INTEGRA1:14, INTEGRA1:16;
hence h | (divset D,k) is bounded ; :: thesis: verum

end;

then reconsider h = h as Function of (divset D,k),REAL ;
for x1, x2 being Real st x1 in divset D,k & x2 in divset D,k holds
abs ((h . x1) - (h . x2)) <= r1

proof

let x1, x2 be Real; :: thesis: ( x1 in divset D,k & x2 in divset D,k implies abs ((h . x1) - (h . x2)) <= r1 )
assume A26: ( x1 in divset D,k & x2 in divset D,k ) ; :: thesis: abs ((h . x1) - (h . x2)) <= r1
A27: abs (x1 - x2) <= (delta T) . m

proof

now

per cases ( x1 >= x2 or x1 < x2 ) ;

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

then x1 - x2 >= 0 by XREAL_1:50;
then A28: abs (x1 - x2) = x1 - x2 by ABSVALUE:def 1;
( x1 <= sup (divset D,k) & x2 >= inf (divset D,k) ) by A26, INTEGRA2:1;
then abs (x1 - x2) <= (sup (divset D,k)) - (inf (divset D,k)) by A28, XREAL_1:15;
then A29: abs (x1 - x2) <= vol (divset D,k) by INTEGRA1:def 6;
A30: k in Seg (len D) by A24, FINSEQ_1:def 3;
then k in dom D by FINSEQ_1:def 3;
then A31: (upper_volume (chi A,A),D) . k = vol (divset D,k) by INTEGRA1:22;
k in Seg (len (upper_volume (chi A,A),D)) by A30, INTEGRA1:def 7;
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 5;
then (upper_volume (chi A,A),D) . k <= max (rng (upper_volume (chi A,A),D)) by XXREAL_2:def 8;
then (upper_volume (chi A,A),D) . k <= delta (T . m) by INTEGRA1:def 19;
then abs (x1 - x2) <= delta (T . m) by A29, A31, XXREAL_0:2;
hence abs (x1 - x2) <= (delta T) . m by INTEGRA2:def 3; :: thesis: verum

end;

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

then x1 - x2 < 0 by XREAL_1:51;
then abs (x1 - x2) = - (x1 - x2) by ABSVALUE:def 1;
then A32: abs (x1 - x2) = x2 - x1 ;
( x2 <= sup (divset D,k) & x1 >= inf (divset D,k) ) by A26, INTEGRA2:1;
then abs (x1 - x2) <= (sup (divset D,k)) - (inf (divset D,k)) by A32, XREAL_1:15;
then A33: abs (x1 - x2) <= vol (divset D,k) by INTEGRA1:def 6;
A34: k in Seg (len D) by A24, FINSEQ_1:def 3;
then k in dom D by FINSEQ_1:def 3;
then A35: (upper_volume (chi A,A),D) . k = vol (divset D,k) by INTEGRA1:22;
k in Seg (len (upper_volume (chi A,A),D)) by A34, INTEGRA1:def 7;
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 5;
then (upper_volume (chi A,A),D) . k <= max (rng (upper_volume (chi A,A),D)) by XXREAL_2:def 8;
then (upper_volume (chi A,A),D) . k <= delta (T . m) by INTEGRA1:def 19;
then abs (x1 - x2) <= delta (T . m) by A33, A35, XXREAL_0:2;
hence abs (x1 - x2) <= (delta T) . m by INTEGRA2:def 3; :: thesis: verum

end;

end;

end;

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

end;

((delta T) . m) - 0 >= 0

proof

A36: (delta T) . m = delta D by INTEGRA2:def 3
.= max (rng (upper_volume (chi A,A),D)) by INTEGRA1:def 19 ;
A37: k in Seg (len D) by A24, FINSEQ_1:def 3;
then k in dom D by FINSEQ_1:def 3;
then (upper_volume (chi A,A),D) . k = vol (divset D,k) by INTEGRA1:22;
then A38: (upper_volume (chi A,A),D) . k >= 0 by INTEGRA1:11;
k in Seg (len (upper_volume (chi A,A),D)) by A37, INTEGRA1:def 7;
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 5;
hence ((delta T) . m) - 0 >= 0 by A36, A38, XXREAL_2:def 8; :: thesis: verum

end;

then A39: abs (x1 - x2) <= abs (((delta T) . m) - 0 ) by A27, ABSVALUE:def 1;
abs (((delta T) . m) - 0 ) < s by A20, A22;
then A40: abs (x1 - x2) < s by A39, XXREAL_0:2;
A41: ( x1 in dom h & x2 in dom h ) by A26, PARTFUN1:def 4;
dom h = (dom g) /\ (divset D,k) by RELAT_1:90;
then A42: dom h c= dom g by XBOOLE_1:17;
then X: ( x1 in dom g & x2 in dom g ) by A41;
( g . x1 = h . x1 & g . x2 = h . x2 ) by A41, FUNCT_1:70;
then ( f . x1 = h . x1 & f . x2 = h . x2 ) by A41, A42, FUNCT_1:70;
hence abs ((h . x1) - (h . x2)) <= r1 by A19, A40, X; :: thesis: verum

end;

then A43: (sup (rng (g | (divset D,k)))) - (inf (rng (g | (divset D,k)))) <= r1 by INTEGRA4:24;
vol (divset D,k) >= 0 by INTEGRA1:11;
then ((sup (rng (g | (divset D,k)))) - (inf (rng (g | (divset D,k))))) * (vol (divset D,k)) <= r1 * (vol (divset D,k)) by A43, XREAL_1:66;
then A44: ((sup (rng (g | (divset D,k)))) * (vol (divset D,k))) - ((inf (rng (g | (divset D,k)))) * (vol (divset D,k))) <= r1 * (vol (divset D,k)) ;
k in Seg (len D) by A24, FINSEQ_1:def 3;
then B45: k in dom D by FINSEQ_1:def 3;
then ((upper_volume g,D) . k) - ((inf (rng (g | (divset D,k)))) * (vol (divset D,k))) <= r1 * (vol (divset D,k)) by A44, INTEGRA1:def 7;
then ((upper_volume g,D) . k) - ((lower_volume g,D) . k) <= r1 * (vol (divset D,k)) by B45, INTEGRA1:def 8;
hence ((upper_volume g,D) . k) - ((lower_volume g,D) . k) <= r1 * ((upper_volume (chi A,A),D) . k) by B45, INTEGRA1:22; :: thesis: verum

end;

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;
for k being Nat st k in Seg (len D) holds
OSC . k <= (r1 * VOL) . k

proof

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 A46: 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 A23, A46;
hence OSC . k <= (r1 * VOL) . k by RVSUM_1:67; :: thesis: verum

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: verum

end;

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

proof

let m be Element of NAT ; :: thesis: ( n <= m implies abs ((osc . m) - 0 ) < r )
assume n <= m ; :: thesis: abs ((osc . m) - 0 ) < r
then ((upper_sum g,T) . m) - ((lower_sum g,T) . m) <= r1 * (vol A) by A21;
then A47: ((upper_sum g,T) . m) - ((lower_sum g,T) . m) < r by A18, XXREAL_0:2;
A48: 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) ;
reconsider D = T . m as Division of A ;
upper_sum g,D >= lower_sum g,D by A4, 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 ((upper_sum g,T) . m) - ((lower_sum g,T) . m) >= 0 by XREAL_1:50;
hence abs ((osc . m) - 0 ) < r by A47, A48, ABSVALUE:def 1; :: thesis: verum

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: verum

end;

then osc is convergent by SEQ_2:def 6;
then A49: lim osc = 0 by A12, SEQ_2:def 7;
( upper_sum g,T is convergent & lower_sum g,T is convergent ) by A4, A10, A11, INTEGRA4:8, INTEGRA4:9;
hence (lim (upper_sum g,T)) - (lim (lower_sum g,T)) = 0 by A49, SEQ_2:26; :: thesis: verum

end;

then g is integrable by A4, INTEGRA4:12;
then consider g being PartFunc of A,REAL such that
A50: ( g = f | A & g is integrable ) ;
thus f is_integrable_on A by A50, Def2; :: thesis: verum