let A be closed-interval Subset of REAL ; :: thesis:
let f be PartFunc of REAL ,REAL ; :: thesis:
assume that
A1: f | A is non-decreasing and
A2: A c= dom f ; :: thesis:
A3: for D being Division of A
for k being Element of NAT st k in dom D holds
( 0 <= ((upper_volume (f || A),D) . k) - ((lower_volume (f || A),D) . k) & ((upper_volume (f || A),D) . k) - ((lower_volume (f || A),D) . k) <= ((f . (sup (divset D,k))) - (f . (inf (divset D,k)))) * (delta D) )

proof

end;

A14: for D being Division of A holds
( (upper_sum (f || A),D) - (lower_sum (f || A),D) <= (delta D) * ((f . (sup A)) - (f . (inf A))) & (upper_sum (f || A),D) - (lower_sum (f || A),D) >= 0 )

proof

let D be Division of A; :: thesis:
deffunc H₁( Nat) -> Element of REAL = f . (sup (divset D,$1));
consider F1 being FinSequence of REAL such that
A15: ( len F1 = len D & ( for i being Nat st i in dom F1 holds
F1 . i = H₁(i) ) ) from FINSEQ_2:sch 1();
(len D) - 1 in NAT

proof

ex j being Nat st len D = 1 + j by NAT_1:10, NAT_1:14;
hence (len D) - 1 in NAT by ORDINAL1:def 13; :: thesis:

end;

then consider k1 being Element of NAT such that
A16: k1 = (len D) - 1 ;
deffunc H₂( Nat) -> Element of REAL = f . (inf (divset D,$1));
consider F2 being FinSequence of REAL such that
A17: ( len F2 = len D & ( for i being Nat st i in dom F2 holds
F2 . i = H₂(i) ) ) from FINSEQ_2:sch 1();
deffunc H₃( Nat) -> Element of REAL = f . (sup (divset D,$1));
A18: dom F2 = Seg (len D) by A17, FINSEQ_1:def 3;
consider F being FinSequence of REAL such that
A19: ( len F = k1 & ( for i being Nat st i in dom F holds
F . i = H₃(i) ) ) from FINSEQ_2:sch 1();
A20: dom F = Seg k1 by A19, FINSEQ_1:def 3;
A21: for i being Nat st 1 <= i & i <= len F2 holds
F2 . i = (<*(f . (inf A))*> ^ F) . i

proof

let i be Nat; :: thesis:
assume that
A22: 1 <= i and
A23: i <= len F2 ; :: thesis:

per cases ;

suppose A24: i = 1 ; :: thesis:

A25: i in Seg (len D) by A17, A22, A23, FINSEQ_1:3;
then A26: i in dom D by FINSEQ_1:def 3;
F2 . i = f . (inf (divset D,i)) by A17, A18, A25
.= f . (inf A) by A24, A26, INTEGRA1:def 5 ;
hence F2 . i = (<*(f . (inf A))*> ^ F) . i by A24, FINSEQ_1:58; :: thesis:

end;

suppose A27: i <> 1 ; :: thesis:

then A28: i > 1 by A22, XXREAL_0:1;
then 1 + 1 <= i by NAT_1:13;
then A29: (len <*(f . (inf A))*>) + 1 <= i by FINSEQ_1:56;
A30: i in Seg (len D) by A17, A22, A23, FINSEQ_1:3;
then A31: i in dom D by FINSEQ_1:def 3;
then reconsider k2 = i - 1 as Element of NAT by A27, INTEGRA1:9;
1 + 1 <= k2 + 1 by A28, NAT_1:13;
then A32: 1 <= k2 by XREAL_1:21;
k2 + 1 <= len F2 by A23;
then A33: k2 <= (len D) - 1 by A17, XREAL_1:21;
then A34: k2 in Seg k1 by A16, A32, FINSEQ_1:3;
A35: sup (divset D,k2) = D . (i - 1)

proof

len D <= (len D) + 1 by NAT_1:13;
then (len D) - 1 <= len D by XREAL_1:22;
then k2 <= len D by A33, XXREAL_0:2;
then k2 in Seg (len D) by A32, FINSEQ_1:3;
then A36: k2 in dom D by FINSEQ_1:def 3;

per cases ;

suppose k2 = 1 ; :: thesis:

hence sup (divset D,k2) = D . (i - 1) by A36, INTEGRA1:def 5; :: thesis:

end;

suppose k2 <> 1 ; :: thesis:

hence sup (divset D,k2) = D . (i - 1) by A36, INTEGRA1:def 5; :: thesis:

end;

len F2 = 1 + ((len D) - 1) by A17
.= (len <*(f . (inf A))*>) + (len F) by A16, A19, FINSEQ_1:56 ;
then A37: (<*(f . (inf A))*> ^ F) . i = F . (i - (len <*(f . (inf A))*>)) by A23, A29, FINSEQ_1:36
.= F . (i - 1) by FINSEQ_1:56 ;
F2 . i = f . (inf (divset D,i)) by A17, A18, A30
.= f . (D . (i - 1)) by A27, A31, INTEGRA1:def 5 ;
hence F2 . i = (<*(f . (inf A))*> ^ F) . i by A19, A20, A37, A34, A35; :: thesis:

end;

len (<*(f . (inf A))*> ^ F) = (len <*(f . (inf A))*>) + (len F) by FINSEQ_1:35
.= 1 + ((len D) - 1) by A16, A19, FINSEQ_1:56
.= len D ;
then A38: F2 = <*(f . (inf A))*> ^ F by A17, A21, FINSEQ_1:18;
( len (upper_volume (f || A),D) = len D & len (lower_volume (f || A),D) = len D ) by INTEGRA1:def 7, INTEGRA1:def 8;
then A39: Sum ((upper_volume (f || A),D) - (lower_volume (f || A),D)) = (Sum (upper_volume (f || A),D)) - (Sum (lower_volume (f || A),D)) by Th2
.= (upper_sum (f || A),D) - (Sum (lower_volume (f || A),D)) by INTEGRA1:def 9
.= (upper_sum (f || A),D) - (lower_sum (f || A),D) by INTEGRA1:def 10 ;
A40: dom F1 = Seg (len D) by A15, FINSEQ_1:def 3;
A41: for i being Nat st 1 <= i & i <= len F1 holds
F1 . i = (F ^ <*(f . (sup A))*>) . i

proof

let i be Nat; :: thesis:
assume that
A42: 1 <= i and
A43: i <= len F1 ; :: thesis:

now

per cases ;

suppose i <= len F ; :: thesis:

then i in Seg (len F) by A42, FINSEQ_1:3;
then A44: ( F . i = f . (sup (divset D,i)) & i in dom F ) by A19, A20, FINSEQ_1:def 3;
i in Seg (len F1) by A42, A43, FINSEQ_1:3;
then F1 . i = f . (sup (divset D,i)) by A15, A40;
hence F1 . i = (F ^ <*(f . (sup A))*>) . i by A44, FINSEQ_1:def 7; :: thesis:

end;

suppose i > len F ; :: thesis:

then A45: i >= (len F) + 1 by NAT_1:13;
then A46: i = (len F) + 1 by A15, A16, A19, A43, XXREAL_0:1;
A47: i in Seg (len F1) by A42, A43, FINSEQ_1:3;
then A48: i in dom D by A15, FINSEQ_1:def 3;
A49: sup (divset D,i) = D . i

proof

now

per cases ;

suppose i = 1 ; :: thesis:

hence sup (divset D,i) = D . i by A48, INTEGRA1:def 5; :: thesis:

end;

suppose i <> 1 ; :: thesis:

hence sup (divset D,i) = D . i by A48, INTEGRA1:def 5; :: thesis:

end;

hence sup (divset D,i) = D . i ; :: thesis:

end;

F1 . i = f . (sup (divset D,i)) by A15, A40, A47;
then F1 . i = f . (D . (len D)) by A15, A16, A19, A43, A45, A49, XXREAL_0:1
.= f . (sup A) by INTEGRA1:def 2 ;
hence F1 . i = (F ^ <*(f . (sup A))*>) . i by A46, FINSEQ_1:59; :: thesis:

end;

hence F1 . i = (F ^ <*(f . (sup A))*>) . i ; :: thesis:

end;

( len (upper_volume (f || A),D) = len D & len (lower_volume (f || A),D) = len D ) by INTEGRA1:def 7, INTEGRA1:def 8;
then A50: len ((upper_volume (f || A),D) - (lower_volume (f || A),D)) = len D by Th2;
A51: len (F1 - F2) = len D by A15, A17, Th2;
A52: for k being Element of NAT st k in dom ((upper_volume (f || A),D) - (lower_volume (f || A),D)) holds
((upper_volume (f || A),D) - (lower_volume (f || A),D)) . k <= ((delta D) * (F1 - F2)) . k

proof

end;

(delta D) * (F1 - F2) = ((delta D) multreal ) * (F1 - F2) by RVSUM_1:def 7;
then len ((delta D) * (F1 - F2)) = len (F1 - F2) by FINSEQ_2:37;
then len ((upper_volume (f || A),D) - (lower_volume (f || A),D)) = len ((delta D) * (F1 - F2)) by A15, A17, A50, Th2;
then A57: Sum ((upper_volume (f || A),D) - (lower_volume (f || A),D)) <= Sum ((delta D) * (F1 - F2)) by A52, Th3;
len (F ^ <*(f . (sup A))*>) = (len F) + (len <*(f . (sup A))*>) by FINSEQ_1:35
.= ((len D) - 1) + 1 by A16, A19, FINSEQ_1:56
.= len D ;
then F1 = F ^ <*(f . (sup A))*> by A15, A41, FINSEQ_1:18;
then Sum (F1 - F2) = (f . (sup A)) - (f . (inf A)) by A38, Th1;
hence (upper_sum (f || A),D) - (lower_sum (f || A),D) <= (delta D) * ((f . (sup A)) - (f . (inf A))) by A39, A57, RVSUM_1:117; :: thesis:
for k being Nat st k in dom ((upper_volume (f || A),D) - (lower_volume (f || A),D)) holds
0 <= ((upper_volume (f || A),D) - (lower_volume (f || A),D)) . k

proof

end;

hence (upper_sum (f || A),D) - (lower_sum (f || A),D) >= 0 by A39, RVSUM_1:114; :: thesis:

end;

A61: ( f || A is total & (f || A) | A is bounded )

proof

consider x being Real such that
A62: x in A by SUBSET_1:10;
A63: dom (f || A) = (dom f) /\ A by RELAT_1:90
.= A by A2, XBOOLE_1:28 ;
hence f || A is total by PARTFUN1:def 4; :: thesis:
( inf A <= x & x <= sup A ) by A62, INTEGRA2:1;
then A64: inf A <= sup A by XXREAL_0:2;
for x being set st x in A /\ (dom (f || A)) holds
(f || A) . x >= (f || A) . (inf A)

proof

inf A in A by A64, INTEGRA2:1;
then A65: ( inf A in A /\ (dom f) & f . (inf A) = (f | A) . (inf A) ) by A2, A63, FUNCT_1:70, XBOOLE_1:28;
let x be set ; :: thesis:
assume A66: x in A /\ (dom (f || A)) ; :: thesis:
then x in A ;
then A67: x in A /\ (dom f) by A2, XBOOLE_1:28;
reconsider x = x as Element of A by A66;
( x >= inf A & f . x = (f | A) . x ) by A63, FUNCT_1:70, INTEGRA2:1;
hence (f || A) . x >= (f || A) . (inf A) by A1, A67, A65, RFUNCT_2:48; :: thesis:

end;

then A68: (f || A) | A is bounded_below by RFUNCT_1:88;
for x being set st x in A /\ (dom (f || A)) holds
(f || A) . x <= (f || A) . (sup A)

proof

sup A in A by A64, INTEGRA2:1;
then A69: ( sup A in A /\ (dom f) & f . (sup A) = (f | A) . (sup A) ) by A2, A63, FUNCT_1:70, XBOOLE_1:28;
let x be set ; :: thesis:
assume A70: x in A /\ (dom (f || A)) ; :: thesis:
then x in A ;
then A71: x in A /\ (dom f) by A2, XBOOLE_1:28;
reconsider x = x as Element of A by A70;
( x <= sup A & f . x = (f | A) . x ) by A63, FUNCT_1:70, INTEGRA2:1;
hence (f || A) . x <= (f || A) . (sup A) by A1, A71, A69, RFUNCT_2:48; :: thesis:

end;

then (f || A) | A is bounded_above by RFUNCT_1:87;
hence (f || A) | A is bounded by A68; :: thesis:

end;

for T being DivSequence of A st delta T is convergent & lim (delta T) = 0 holds
(lim (upper_sum (f || A),T)) - (lim (lower_sum (f || A),T)) = 0

proof

let T be DivSequence of A; :: thesis:
assume A72: ( delta T is convergent & lim (delta T) = 0 ) ; :: thesis:
A73: 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 ((((upper_sum (f || A),T) - (lower_sum (f || A),T)) . m) - 0 ) < r

proof

consider x being Real such that
A74: x in A by SUBSET_1:10;
A75: A = A /\ (dom f) by A2, XBOOLE_1:28;
let r be real number ; :: thesis:
assume A76: 0 < r ; :: thesis:
( inf A <= x & x <= sup A ) by A74, INTEGRA2:1;
then A77: inf A <= sup A by XXREAL_0:2;
then ( inf A in A & sup A in A ) by INTEGRA2:1;
then A78: f . (inf A) <= f . (sup A) by A1, A77, A75, RFUNCT_2:48;

now

per cases by A78, XXREAL_0:1;

suppose A79: f . (inf A) = f . (sup A) ; :: thesis:

for m being Element of NAT st 0 <= m holds
abs ((((upper_sum (f || A),T) - (lower_sum (f || A),T)) . m) - 0 ) < r

proof

let m be Element of NAT ; :: thesis:
assume 0 <= m ; :: thesis:
reconsider D1 = T . m as Division of A ;
A80: ((upper_sum (f || A),T) - (lower_sum (f || A),T)) . m = ((upper_sum (f || A),T) . m) + ((- (lower_sum (f || A),T)) . m) by SEQ_1:11
.= ((upper_sum (f || A),T) . m) + (- ((lower_sum (f || A),T) . m)) by SEQ_1:14
.= (upper_sum (f || A),D1) + (- ((lower_sum (f || A),T) . m)) by INTEGRA2:def 4
.= (upper_sum (f || A),D1) + (- (lower_sum (f || A),D1)) by INTEGRA2:def 5 ;
( (upper_sum (f || A),D1) - (lower_sum (f || A),D1) <= (delta D1) * ((f . (sup A)) - (f . (inf A))) & (upper_sum (f || A),D1) - (lower_sum (f || A),D1) >= 0 ) by A14;
hence abs ((((upper_sum (f || A),T) - (lower_sum (f || A),T)) . m) - 0 ) < r by A76, A79, A80, ABSVALUE:def 1; :: thesis:

end;

hence ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((((upper_sum (f || A),T) - (lower_sum (f || A),T)) . m) - 0 ) < r ; :: thesis:

end;

suppose f . (inf A) < f . (sup A) ; :: thesis:

then A81: (f . (sup A)) - (f . (inf A)) > 0 by XREAL_1:52;
then r / ((f . (sup A)) - (f . (inf A))) > 0 by A76, XREAL_1:141;
then consider n being Element of NAT such that
A82: for m being Element of NAT st n <= m holds
abs (((delta T) . m) - 0 ) < r / ((f . (sup A)) - (f . (inf A))) by A72, SEQ_2:def 7;
A83: for m being Element of NAT st n <= m holds
(delta T) . m < r / ((f . (sup A)) - (f . (inf A)))

proof

let m be Element of NAT ; :: thesis:
assume n <= m ; :: thesis:
then A84: abs (((delta T) . m) - 0 ) < r / ((f . (sup A)) - (f . (inf A))) by A82;
(delta T) . m <= abs ((delta T) . m) by ABSVALUE:11;
hence (delta T) . m < r / ((f . (sup A)) - (f . (inf A))) by A84, XXREAL_0:2; :: thesis:

end;

for m being Element of NAT st n <= m holds
abs ((((upper_sum (f || A),T) - (lower_sum (f || A),T)) . m) - 0 ) < r

proof

let m be Element of NAT ; :: thesis:
reconsider D = T . m as Division of A ;
A85: abs ((upper_sum (f || A),D) - (lower_sum (f || A),D)) = abs ((((upper_sum (f || A),T) . m) - (lower_sum (f || A),D)) - 0 ) by INTEGRA2:def 4
.= abs ((((upper_sum (f || A),T) . m) - ((lower_sum (f || A),T) . m)) - 0 ) by INTEGRA2:def 5
.= abs ((((upper_sum (f || A),T) . m) + (- ((lower_sum (f || A),T) . m))) - 0 )
.= abs ((((upper_sum (f || A),T) . m) + ((- (lower_sum (f || A),T)) . m)) - 0 ) by SEQ_1:14
.= abs ((((upper_sum (f || A),T) - (lower_sum (f || A),T)) . m) - 0 ) by SEQ_1:11 ;
assume n <= m ; :: thesis:
then (delta T) . m < r / ((f . (sup A)) - (f . (inf A))) by A83;
then ((delta T) . m) * ((f . (sup A)) - (f . (inf A))) < r by A81, XREAL_1:81;
then A86: (delta D) * ((f . (sup A)) - (f . (inf A))) < r by INTEGRA2:def 3;
(upper_sum (f || A),D) - (lower_sum (f || A),D) <= (delta D) * ((f . (sup A)) - (f . (inf A))) by A14;
then A87: (upper_sum (f || A),D) - (lower_sum (f || A),D) < r by A86, XXREAL_0:2;
(upper_sum (f || A),D) - (lower_sum (f || A),D) >= 0 by A14;
hence abs ((((upper_sum (f || A),T) - (lower_sum (f || A),T)) . m) - 0 ) < r by A87, A85, ABSVALUE:def 1; :: thesis:

end;

hence ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((((upper_sum (f || A),T) - (lower_sum (f || A),T)) . m) - 0 ) < r ; :: thesis:

end;

hence ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((((upper_sum (f || A),T) - (lower_sum (f || A),T)) . m) - 0 ) < r ; :: thesis:

end;

A88: ( upper_sum (f || A),T is convergent & lower_sum (f || A),T is convergent ) by A61, A72, INTEGRA4:8, INTEGRA4:9;
then (upper_sum (f || A),T) - (lower_sum (f || A),T) is convergent by SEQ_2:25;
then lim ((upper_sum (f || A),T) - (lower_sum (f || A),T)) = 0 by A73, SEQ_2:def 7;
hence (lim (upper_sum (f || A),T)) - (lim (lower_sum (f || A),T)) = 0 by A88, SEQ_2:26; :: thesis:

end;

then f || A is integrable by A61, INTEGRA4:12;
hence f is_integrable_on A by Def2; :: thesis: