let A be non empty 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 . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k))))) * (delta D) )

proof

let D be Division of A; :: thesis:
let k be Element of NAT ; :: thesis:
assume A4: k in dom D ; :: thesis:
then A5: ( (upper_volume ((f || A),D)) . k = (upper_bound (rng ((f || A) | (divset (D,k))))) * (vol (divset (D,k))) & (lower_volume ((f || A),D)) . k = (lower_bound (rng ((f || A) | (divset (D,k))))) * (vol (divset (D,k))) ) by INTEGRA1:def 6, INTEGRA1:def 7;
k in Seg (len D) by A4, FINSEQ_1:def 3;
then k in Seg (len (upper_volume ((chi (A,A)),D))) by INTEGRA1:def 6;
then A6: k in dom (upper_volume ((chi (A,A)),D)) by FINSEQ_1:def 3;
vol (divset (D,k)) = (upper_volume ((chi (A,A)),D)) . k by A4, INTEGRA1:20;
then vol (divset (D,k)) in rng (upper_volume ((chi (A,A)),D)) by A6, FUNCT_1:def 3;
then vol (divset (D,k)) <= max (rng (upper_volume ((chi (A,A)),D))) by XXREAL_2:def 8;
then A7: vol (divset (D,k)) <= delta D by INTEGRA3:def 1;
A8: divset (D,k) c= A by A4, INTEGRA1:8;
then A9: divset (D,k) c= dom f by A2, XBOOLE_1:1;
f | (divset (D,k)) is non-decreasing by A1, A4, INTEGRA1:8, RFUNCT_2:30;
then A10: ( lower_bound (rng (f | (divset (D,k)))) = f . (lower_bound (divset (D,k))) & upper_bound (rng (f | (divset (D,k)))) = f . (upper_bound (divset (D,k))) ) by A9, Th15;
dom (f | (divset (D,k))) = (dom f) /\ (divset (D,k)) by RELAT_1:61
.= divset (D,k) by A2, A8, XBOOLE_1:1, XBOOLE_1:28 ;
then A11: rng (f | (divset (D,k))) <> {} by RELAT_1:42;
A12: rng (f | (divset (D,k))) = rng ((f || A) | (divset (D,k))) by A8, FUNCT_1:51;
rng (f | A) is real-bounded by A1, A2, Th14;
then rng (f | (divset (D,k))) is real-bounded by A12, RELAT_1:70, XXREAL_2:45;
then A13: (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) >= 0 by A10, A11, SEQ_4:11, XREAL_1:48;
vol (divset (D,k)) >= 0 by INTEGRA1:9;
then 0 * (vol (divset (D,k))) <= ((f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k))))) * (vol (divset (D,k))) by A13;
hence 0 <= ((upper_volume ((f || A),D)) . k) - ((lower_volume ((f || A),D)) . k) by A10, A5, A12; :: thesis:
((upper_volume ((f || A),D)) . k) - ((lower_volume ((f || A),D)) . k) = ((f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k))))) * (vol (divset (D,k))) by A10, A5, A12;
hence ((upper_volume ((f || A),D)) . k) - ((lower_volume ((f || A),D)) . k) <= ((f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k))))) * (delta D) by A13, A7, XREAL_1:64; :: thesis:

end;

A14: for D being Division of A holds
( (upper_sum ((f || A),D)) - (lower_sum ((f || A),D)) <= (delta D) * ((f . (upper_bound A)) - (f . (lower_bound 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 = In ((f . (upper_bound (divset (D,$1)))),REAL);
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 12; :: thesis:

end;

then consider k1 being Element of NAT such that
A16: k1 = (len D) - 1 ;
deffunc H₂( Nat) -> Element of REAL = In ((f . (lower_bound (divset (D,$1)))),REAL);
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 = In ((f . (upper_bound (divset (D,$1)))),REAL);
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 . (lower_bound 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:1;
then A26: i in dom D by FINSEQ_1:def 3;
F2 . i = H₂(i) by A17, A18, A25
.= f . (lower_bound (divset (D,i)))
.= f . (lower_bound A) by A24, A26, INTEGRA1:def 4 ;
hence F2 . i = (<*(f . (lower_bound A))*> ^ F) . i by A24, FINSEQ_1:41; :: 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 . (lower_bound A))*>) + 1 <= i by FINSEQ_1:39;
A30: i in Seg (len D) by A17, A22, A23, FINSEQ_1:1;
then A31: i in dom D by FINSEQ_1:def 3;
then reconsider k2 = i - 1 as Element of NAT by A27, INTEGRA1:7;
1 + 1 <= k2 + 1 by A28, NAT_1:13;
then A32: 1 <= k2 by XREAL_1:19;
k2 + 1 <= len F2 by A23;
then A33: k2 <= (len D) - 1 by A17, XREAL_1:19;
then A34: k2 in Seg k1 by A16, A32, FINSEQ_1:1;
A35: upper_bound (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:20;
then k2 <= len D by A33, XXREAL_0:2;
then k2 in Seg (len D) by A32, FINSEQ_1:1;
then A36: k2 in dom D by FINSEQ_1:def 3;

per cases ;

suppose k2 = 1 ; :: thesis:

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

end;

suppose k2 <> 1 ; :: thesis:

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

end;

len F2 = 1 + ((len D) - 1) by A17
.= (len <*(f . (lower_bound A))*>) + (len F) by A16, A19, FINSEQ_1:39 ;
then A37: (<*(f . (lower_bound A))*> ^ F) . i = F . (i - (len <*(f . (lower_bound A))*>)) by A23, A29, FINSEQ_1:23
.= F . (i - 1) by FINSEQ_1:39 ;
F2 . i = H₂(i) by A17, A18, A30
.= f . (lower_bound (divset (D,i)))
.= f . (upper_bound (divset (D,k2))) by A27, A31, INTEGRA1:def 4, A35
.= H₃(k2) ;
hence F2 . i = (<*(f . (lower_bound A))*> ^ F) . i by A19, A20, A37, A34; :: thesis:

end;

len (<*(f . (lower_bound A))*> ^ F) = (len <*(f . (lower_bound A))*>) + (len F) by FINSEQ_1:22
.= 1 + ((len D) - 1) by A16, A19, FINSEQ_1:39
.= len D ;
then A38: F2 = <*(f . (lower_bound A))*> ^ F by A17, A21, FINSEQ_1:14;
( len (upper_volume ((f || A),D)) = len D & len (lower_volume ((f || A),D)) = len D ) by INTEGRA1:def 6, INTEGRA1:def 7;
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 8
.= (upper_sum ((f || A),D)) - (lower_sum ((f || A),D)) by INTEGRA1:def 9 ;
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 . (upper_bound A))*>) . i

proof

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

now :: thesis:

per cases ;

suppose i <= len F ; :: thesis:

then A44: i in Seg (len F) by A42, FINSEQ_1:1;
then A45: F . i = H₃(i) by A19, A20
.= f . (upper_bound (divset (D,i))) ;
A46: i in dom F by A19, A20, A44;
i in Seg (len F1) by A42, A43, FINSEQ_1:1;
then F1 . i = H₁(i) by A15, A40
.= f . (upper_bound (divset (D,i))) ;
hence F1 . i = (F ^ <*(f . (upper_bound A))*>) . i by A46, A45, FINSEQ_1:def 7; :: thesis:

end;

suppose i > len F ; :: thesis:

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

proof

now :: thesis:

per cases ;

suppose i = 1 ; :: thesis:

hence upper_bound (divset (D,i)) = D . i by A50, INTEGRA1:def 4; :: thesis:

end;

suppose i <> 1 ; :: thesis:

hence upper_bound (divset (D,i)) = D . i by A50, INTEGRA1:def 4; :: thesis:

end;

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

end;

F1 . i = H₁(i) by A15, A40, A49
.= f . (upper_bound (divset (D,i))) ;
then F1 . i = f . (D . (len D)) by A15, A16, A19, A43, A47, A51, XXREAL_0:1
.= f . (upper_bound A) by INTEGRA1:def 2 ;
hence F1 . i = (F ^ <*(f . (upper_bound A))*>) . i by A48, FINSEQ_1:42; :: thesis:

end;

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

end;

( len (upper_volume ((f || A),D)) = len D & len (lower_volume ((f || A),D)) = len D ) by INTEGRA1:def 6, INTEGRA1:def 7;
then A52: len ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) = len D by Th2;
A53: len (F1 - F2) = len D by A15, A17, Th2;
A54: 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;

proof

end;

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

end;

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

proof

consider x being Element of REAL such that
A65: x in A by SUBSET_1:4;
A66: dom (f || A) = (dom f) /\ A by RELAT_1:61
.= A by A2, XBOOLE_1:28 ;
hence f || A is total by PARTFUN1:def 2; :: thesis:
( lower_bound A <= x & x <= upper_bound A ) by A65, INTEGRA2:1;
then A67: lower_bound A <= upper_bound A by XXREAL_0:2;
for x being object st x in A /\ (dom (f || A)) holds
(f || A) . x >= (f || A) . (lower_bound A)

proof

lower_bound A in A by A67, INTEGRA2:1;
then A68: ( lower_bound A in A /\ (dom f) & f . (lower_bound A) = (f | A) . (lower_bound A) ) by A2, A66, FUNCT_1:47, XBOOLE_1:28;
let x be object ; :: thesis:
assume A69: x in A /\ (dom (f || A)) ; :: thesis:
then x in A ;
then A70: x in A /\ (dom f) by A2, XBOOLE_1:28;
reconsider x = x as Element of A by A69;
( x >= lower_bound A & f . x = (f | A) . x ) by A66, FUNCT_1:47, INTEGRA2:1;
hence (f || A) . x >= (f || A) . (lower_bound A) by A1, A70, A68, RFUNCT_2:24; :: thesis:

end;

then A71: (f || A) | A is bounded_below by RFUNCT_1:71;
for x being object st x in A /\ (dom (f || A)) holds
(f || A) . x <= (f || A) . (upper_bound A)

proof

upper_bound A in A by A67, INTEGRA2:1;
then A72: ( upper_bound A in A /\ (dom f) & f . (upper_bound A) = (f | A) . (upper_bound A) ) by A2, A66, FUNCT_1:47, XBOOLE_1:28;
let x be object ; :: thesis:
assume A73: x in A /\ (dom (f || A)) ; :: thesis:
then x in A ;
then A74: x in A /\ (dom f) by A2, XBOOLE_1:28;
reconsider x = x as Element of A by A73;
( x <= upper_bound A & f . x = (f | A) . x ) by A66, FUNCT_1:47, INTEGRA2:1;
hence (f || A) . x <= (f || A) . (upper_bound A) by A1, A74, A72, RFUNCT_2:24; :: thesis:

end;

then (f || A) | A is bounded_above by RFUNCT_1:70;
hence (f || A) | A is bounded by A71; :: 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 A75: ( delta T is convergent & lim (delta T) = 0 ) ; :: thesis:
A76: for r being Real st 0 < r holds
ex n being Nat st
for m being Nat st n <= m holds
|.((((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) . m) - 0).| < r

proof

consider x being Element of REAL such that
A77: x in A by SUBSET_1:4;
A78: A = A /\ (dom f) by A2, XBOOLE_1:28;
let r be Real; :: thesis:
assume A79: 0 < r ; :: thesis:
( lower_bound A <= x & x <= upper_bound A ) by A77, INTEGRA2:1;
then A80: lower_bound A <= upper_bound A by XXREAL_0:2;
then ( lower_bound A in A & upper_bound A in A ) by INTEGRA2:1;
then A81: f . (lower_bound A) <= f . (upper_bound A) by A1, A80, A78, RFUNCT_2:24;

per cases by A81, XXREAL_0:1;

suppose A82: f . (lower_bound A) = f . (upper_bound A) ; :: thesis:

reconsider n = 0 as Nat ;
take n ; :: thesis:
let m be Nat; :: thesis:
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
assume n <= m ; :: thesis:
reconsider D1 = T . mm as Division of A ;
A83: ((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:7
.= ((upper_sum ((f || A),T)) . m) + (- ((lower_sum ((f || A),T)) . m)) by SEQ_1:10
.= (upper_sum ((f || A),D1)) + (- ((lower_sum ((f || A),T)) . m)) by INTEGRA2:def 2
.= (upper_sum ((f || A),D1)) + (- (lower_sum ((f || A),D1))) by INTEGRA2:def 3 ;
( (upper_sum ((f || A),D1)) - (lower_sum ((f || A),D1)) <= (delta D1) * ((f . (upper_bound A)) - (f . (lower_bound A))) & (upper_sum ((f || A),D1)) - (lower_sum ((f || A),D1)) >= 0 ) by A14;
hence |.((((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) . m) - 0).| < r by A79, A82, A83, ABSVALUE:def 1; :: thesis:

end;

suppose f . (lower_bound A) < f . (upper_bound A) ; :: thesis:

then A84: (f . (upper_bound A)) - (f . (lower_bound A)) > 0 by XREAL_1:50;
then r / ((f . (upper_bound A)) - (f . (lower_bound A))) > 0 by A79, XREAL_1:139;
then consider n being Nat such that
A85: for m being Nat st n <= m holds
|.(((delta T) . m) - 0).| < r / ((f . (upper_bound A)) - (f . (lower_bound A))) by A75, SEQ_2:def 7;
A86: for m being Element of NAT st n <= m holds
(delta T) . m < r / ((f . (upper_bound A)) - (f . (lower_bound A)))

proof

let m be Element of NAT ; :: thesis:
assume n <= m ; :: thesis:
then A87: |.(((delta T) . m) - 0).| < r / ((f . (upper_bound A)) - (f . (lower_bound A))) by A85;
(delta T) . m <= |.((delta T) . m).| by ABSVALUE:4;
hence (delta T) . m < r / ((f . (upper_bound A)) - (f . (lower_bound A))) by A87, XXREAL_0:2; :: 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 ;
A88: |.((upper_sum ((f || A),D)) - (lower_sum ((f || A),D))).| = |.((((upper_sum ((f || A),T)) . mm) - (lower_sum ((f || A),D))) - 0).| by INTEGRA2:def 2
.= |.((((upper_sum ((f || A),T)) . mm) - ((lower_sum ((f || A),T)) . m)) - 0).| by INTEGRA2:def 3
.= |.((((upper_sum ((f || A),T)) . m) + (- ((lower_sum ((f || A),T)) . m))) - 0).|
.= |.((((upper_sum ((f || A),T)) . m) + ((- (lower_sum ((f || A),T))) . m)) - 0).| by SEQ_1:10
.= |.((((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) . m) - 0).| by SEQ_1:7 ;
assume n <= m ; :: thesis:
then (delta T) . mm < r / ((f . (upper_bound A)) - (f . (lower_bound A))) by A86;
then ((delta T) . m) * ((f . (upper_bound A)) - (f . (lower_bound A))) < r by A84, XREAL_1:79;
then A89: (delta D) * ((f . (upper_bound A)) - (f . (lower_bound A))) < r by INTEGRA3:def 2;
(upper_sum ((f || A),D)) - (lower_sum ((f || A),D)) <= (delta D) * ((f . (upper_bound A)) - (f . (lower_bound A))) by A14;
then A90: (upper_sum ((f || A),D)) - (lower_sum ((f || A),D)) < r by A89, XXREAL_0:2;
(upper_sum ((f || A),D)) - (lower_sum ((f || A),D)) >= 0 by A14;
hence |.((((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) . m) - 0).| < r by A90, A88, ABSVALUE:def 1; :: thesis:

end;

A91: ( upper_sum ((f || A),T) is convergent & lower_sum ((f || A),T) is convergent ) by A64, A75, INTEGRA4:8, INTEGRA4:9;
then (upper_sum ((f || A),T)) - (lower_sum ((f || A),T)) is convergent ;
then lim ((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) = 0 by A76, SEQ_2:def 7;
hence (lim (upper_sum ((f || A),T))) - (lim (lower_sum ((f || A),T))) = 0 by A91, SEQ_2:12; :: thesis:

end;

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