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 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
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;

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: ( 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 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;

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: f is_integrable_on A
then f .: A is 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: ( 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 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 A15: 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:9;

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

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

end;

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

then r / (vol A) > 0 by A15, XREAL_1:139;
then consider r1 being real number such that
A19: 0 < r1 and
A20: r1 < r / (vol A) by XREAL_1:5;
reconsider r1 = r1 as Real by XREAL_0:def 1;
r1 * (vol A) < r by A18, A20, XREAL_1:79;
hence ex r1 being Real st
( r1 > 0 & r1 * (vol A) < r ) by A19; :: 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
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: ( 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 A27: n <= m ; :: thesis: ((upper_sum (g,T)) . m) - ((lower_sum (g,T)) . m) <= r1 * (vol A)
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: ( k in dom D implies ((upper_volume (g,D)) . k) - ((lower_volume (g,D)) . k) <= r1 * ((upper_volume ((chi (A,A)),D)) . k) )
assume A29: 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 A29, 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 ;
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:20;
then A31: (upper_volume ((chi (A,A)),D)) . k >= 0 by INTEGRA1:9;
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 6;
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 3;
dom h = (dom g) /\ (divset (D,k)) by RELAT_1:61;
then A33: 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 abs ((h . x1) - (h . x2)) <= r1 )
assume that
A34: x1 in divset (D,k) and
A35: x2 in divset (D,k) ; :: thesis: abs ((h . x1) - (h . x2)) <= r1
A36: x2 in dom h by A35, PARTFUN1:def 2;
then g . x2 = h . x2 by FUNCT_1:47;
then A37: f . x2 = h . x2 by A36, A33, FUNCT_1:47;
A38: 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:48;
then A39: abs (x1 - x2) = x1 - x2 by ABSVALUE:def 1;
( x1 <= upper_bound (divset (D,k)) & x2 >= lower_bound (divset (D,k)) ) by A34, A35, INTEGRA2:1;
then abs (x1 - x2) <= (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) by A39, XREAL_1:13;
then A40: abs (x1 - x2) <= vol (divset (D,k)) by INTEGRA1:def 5;
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 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 A41: (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 A29, INTEGRA1:20;
then abs (x1 - x2) <= delta (T . m) by A40, A41, XXREAL_0:2;
hence abs (x1 - x2) <= (delta T) . m by INTEGRA3:def 2; :: thesis: verum

end;

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

then x1 - x2 < 0 by XREAL_1:49;
then abs (x1 - x2) = - (x1 - x2) by ABSVALUE:def 1;
then A42: abs (x1 - x2) = x2 - x1 ;
( x2 <= upper_bound (divset (D,k)) & x1 >= lower_bound (divset (D,k)) ) by A34, A35, INTEGRA2:1;
then abs (x1 - x2) <= (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) by A42, XREAL_1:13;
then A43: abs (x1 - x2) <= vol (divset (D,k)) by INTEGRA1:def 5;
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 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 A44: (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 A29, INTEGRA1:20;
then abs (x1 - x2) <= delta (T . m) by A43, A44, XXREAL_0:2;
hence abs (x1 - x2) <= (delta T) . m by INTEGRA3:def 2; :: thesis: verum

end;

end;

end;

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

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 2;
then g . x1 = h . x1 by FUNCT_1:47;
then f . x1 = h . x1 by A47, A33, FUNCT_1:47;
hence abs ((h . x1) - (h . x2)) <= r1 by A24, A46, A47, A36, A33, A37; :: thesis: verum

end;

vol (divset (D,k)) >= 0 by INTEGRA1:9;
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: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 A29, INTEGRA1:def 6;
then ((upper_volume (g,D)) . k) - ((lower_volume (g,D)) . k) <= r1 * (vol (divset (D,k))) by A29, INTEGRA1:def 7;
hence ((upper_volume (g,D)) . k) - ((lower_volume (g,D)) . k) <= r1 * ((upper_volume ((chi (A,A)),D)) . k) by A29, INTEGRA1:20; :: thesis: verum

end;

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 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:27;
then OSC . k <= r1 * (VOL . k) by A28, A48;
hence OSC . k <= (r1 * VOL) . k by RVSUM_1:45; :: thesis: verum

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: 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 )
reconsider D = T . m as Division of A ;
assume n <= m ; :: thesis: abs ((osc . m) - 0) < r
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:28;
then (upper_sum (g,T)) . m >= lower_sum (g,D) by INTEGRA2:def 2;
then (upper_sum (g,T)) . m >= (lower_sum (g,T)) . m by INTEGRA2:def 3;
then A50: ((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 abs ((osc . m) - 0) < r by A49, A50, 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 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:12; :: thesis: verum

end;

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