let A be closed-interval Subset of REAL ; :: thesis:
let X be set ; :: thesis:
let f be PartFunc of REAL ,REAL ; :: thesis:
let D be Division of A; :: thesis:
assume that
A1: A c= X and
A2: f is_differentiable_on X and
A3: (f `| X) | A is bounded ; :: thesis:
X c= dom f by A2, FDIFF_1:def 7;
then X: A c= dom f by A1, XBOOLE_1:1;
A4: for k being Element of NAT st k in dom D holds
ex r being Real st
( r in divset D,k & (f . (sup (divset D,k))) - (f . (inf (divset D,k))) = (diff f,r) * (vol (divset D,k)) )

proof

let k be Element of NAT ; :: thesis:
assume A5: k in dom D ; :: thesis:

now

per cases ;

suppose A6: inf (divset D,k) = sup (divset D,k) ; :: thesis:

then (sup (divset D,k)) - (inf (divset D,k)) = 0 ;
then A7: vol (divset D,k) = 0 by INTEGRA1:def 6;
consider r being Real such that
A8: r = upper_bound (divset D,k) ;
A9: r in divset D,k

proof

consider a, b being Real such that
A10: ( a <= b & a = inf (divset D,k) & b = sup (divset D,k) ) by INTEGRA1:4;
thus r in divset D,k by A8, A10, INTEGRA2:1; :: thesis:

end;

(diff f,r) * (vol (divset D,k)) = 0 by A7;
hence ex r being Real st
( r in divset D,k & (f . (sup (divset D,k))) - (f . (inf (divset D,k))) = (diff f,r) * (vol (divset D,k)) ) by A6, A9; :: thesis:

end;

suppose A11: inf (divset D,k) <> sup (divset D,k) ; :: thesis:

f | X is continuous by A2, FDIFF_1:33;
then A12: f | A is continuous by A1, FCONT_1:17;
A13: divset D,k c= A by A5, INTEGRA1:10;
A14: f | (divset D,k) is continuous by A5, A12, FCONT_1:17, INTEGRA1:10;
consider r1, r2 being Real such that
A15: ( r1 <= r2 & r1 = inf (divset D,k) & r2 = sup (divset D,k) ) by INTEGRA1:4;
A16: inf (divset D,k) < sup (divset D,k) by A11, A15, XXREAL_0:1;
A17: divset D,k = [.(inf (divset D,k)),(sup (divset D,k)).] by INTEGRA1:5;
A18: f | [.(inf (divset D,k)),(sup (divset D,k)).] is continuous by A14, INTEGRA1:5;
A19: ].(inf (divset D,k)),(sup (divset D,k)).[ c= divset D,k by A17, XXREAL_1:25;
then ].(inf (divset D,k)),(sup (divset D,k)).[ c= A by A13, XBOOLE_1:1;
then Q: f is_differentiable_on ].(inf (divset D,k)),(sup (divset D,k)).[ by A1, A2, FDIFF_1:34, XBOOLE_1:1;
[.(inf (divset D,k)),(sup (divset D,k)).] c= dom f by A13, A17, X, XBOOLE_1:1;
then consider r being Real such that
A20: ( r in ].(inf (divset D,k)),(sup (divset D,k)).[ & diff f,r = ((f . (sup (divset D,k))) - (f . (inf (divset D,k)))) / ((upper_bound (divset D,k)) - (lower_bound (divset D,k))) ) by A16, A18, Q, ROLLE:3;
(sup (divset D,k)) - (inf (divset D,k)) > 0 by A16, XREAL_1:52;
then (diff f,r) * ((sup (divset D,k)) - (inf (divset D,k))) = (f . (sup (divset D,k))) - (f . (inf (divset D,k))) by A20, XCMPLX_1:88;
then (diff f,r) * (vol (divset D,k)) = (f . (sup (divset D,k))) - (f . (inf (divset D,k))) by INTEGRA1:def 6;
hence ex r being Real st
( r in divset D,k & (f . (sup (divset D,k))) - (f . (inf (divset D,k))) = (diff f,r) * (vol (divset D,k)) ) by A19, A20; :: thesis:

end;

hence ex r being Real st
( r in divset D,k & (f . (sup (divset D,k))) - (f . (inf (divset D,k))) = (diff f,r) * (vol (divset D,k)) ) ; :: thesis:

end;

A21: for k being Element of NAT
for r being Real st k in dom D & r in divset D,k holds
diff f,r in rng (((f `| X) || A) | (divset D,k))

proof

let k be Element of NAT ; :: thesis:
let r be Real; :: thesis:
assume that
A22: k in dom D and
A23: r in divset D,k ; :: thesis:
A24: divset D,k c= A by A22, INTEGRA1:10;
then divset D,k c= X by A1, XBOOLE_1:1;
then A25: (f `| X) . r = diff f,r by A2, A23, FDIFF_1:def 8;
A26: dom ((f `| X) | A) = (dom (f `| X)) /\ A by RELAT_1:90
.= X /\ A by A2, FDIFF_1:def 8
.= A by A1, XBOOLE_1:28 ;
then A27: diff f,r = ((f `| X) || A) . r by A23, A24, A25, FUNCT_1:70;
A28: dom (((f `| X) || A) | (divset D,k)) = A /\ (divset D,k) by A26, RELAT_1:90
.= divset D,k by A22, INTEGRA1:10, XBOOLE_1:28 ;
then (((f `| X) || A) | (divset D,k)) . r in rng (((f `| X) || A) | (divset D,k)) by A23, FUNCT_1:def 5;
hence diff f,r in rng (((f `| X) || A) | (divset D,k)) by A23, A27, A28, FUNCT_1:70; :: thesis:

end;

A29: for k being Element of NAT st k in dom D holds
rng (((f `| X) || A) | (divset D,k)) is bounded

proof

let k be Element of NAT ; :: thesis:
assume k in dom D ; :: thesis:
dom (f `| X) = X by A2, FDIFF_1:def 8;
then reconsider g = f `| X as PartFunc of X,REAL by RELSET_1:13;
A30: ( (f `| X) | A is bounded_above & (f `| X) | A is bounded_below ) by A3;
then consider r1 being real number such that
A31: for x being set st x in A /\ (dom (f `| X)) holds
(f `| X) . x <= r1 by RFUNCT_1:87;
consider r2 being real number such that
A32: for x being set st x in A /\ (dom (f `| X)) holds
(f `| X) . x >= r2 by A30, RFUNCT_1:88;
A33: dom ((f `| X) | A) = (dom (f `| X)) /\ A by RELAT_1:90;
for x being set st x in A /\ (dom ((f `| X) || A)) holds
((f `| X) || A) . x <= r1

proof

let x be set ; :: thesis:
assume A34: x in A /\ (dom ((f `| X) || A)) ; :: thesis:
A35: A /\ (A /\ (dom (f `| X))) = (A /\ A) /\ (dom (f `| X)) by XBOOLE_1:16
.= A /\ (dom (f `| X)) ;
reconsider y = g . x as Real ;
( y <= r1 & g . x = ((f `| X) || A) . x ) by A31, A33, A34, A35, FUNCT_1:70;
hence ((f `| X) || A) . x <= r1 ; :: thesis:

end;

then ((f `| X) || A) | A is bounded_above by RFUNCT_1:87;
then A36: rng (((f `| X) || A) | (divset D,k)) is bounded_above by INTEGRA4:18;
for x being set st x in A /\ (dom ((f `| X) || A)) holds
((f `| X) || A) . x >= r2

proof

let x be set ; :: thesis:
assume A37: x in A /\ (dom ((f `| X) || A)) ; :: thesis:
A38: A /\ (A /\ (dom (f `| X))) = (A /\ A) /\ (dom (f `| X)) by XBOOLE_1:16
.= A /\ (dom (f `| X)) ;
reconsider y = g . x as Real ;
( y >= r2 & g . x = ((f `| X) || A) . x ) by A32, A33, A37, A38, FUNCT_1:70;
hence ((f `| X) || A) . x >= r2 ; :: thesis:

end;

then ((f `| X) || A) | A is bounded_below by RFUNCT_1:88;
then rng (((f `| X) || A) | (divset D,k)) is bounded_below by INTEGRA4:19;
hence rng (((f `| X) || A) | (divset D,k)) is bounded by A36; :: thesis:

end;

deffunc H₁( Nat) -> Element of REAL = (f . (sup (divset D,$1))) - (f . (inf (divset D,$1)));
consider p being FinSequence of REAL such that
A39: ( len p = len D & ( for i being Nat st i in dom p holds
p . i = H₁(i) ) ) from FINSEQ_2:sch 1();
A40: dom p = Seg (len D) by A39, FINSEQ_1:def 3;
(len D) - 1 in NAT

proof

len D >= 1 by NAT_1:14;
then consider j being Nat such that
A41: len D = 1 + j by NAT_1:10;
thus (len D) - 1 in NAT by A41, ORDINAL1:def 13; :: thesis:

end;

then reconsider k1 = (len D) - 1 as Element of NAT ;
deffunc H₂( Nat) -> Element of REAL = f . (sup (divset D,$1));
consider s1 being FinSequence of REAL such that
A42: ( len s1 = k1 & ( for i being Nat st i in dom s1 holds
s1 . i = H₂(i) ) ) from FINSEQ_2:sch 1();
A43: dom s1 = Seg k1 by A42, FINSEQ_1:def 3;
deffunc H₃( Nat) -> Element of REAL = f . (inf (divset D,($1 + 1)));
consider s2 being FinSequence of REAL such that
A44: ( len s2 = k1 & ( for i being Nat st i in dom s2 holds
s2 . i = H₃(i) ) ) from FINSEQ_2:sch 1();
A45: dom s2 = Seg k1 by A44, FINSEQ_1:def 3;
A46: for i being Element of NAT st i in Seg k1 holds
sup (divset D,i) = inf (divset D,(i + 1))

proof

let i be Element of NAT ; :: thesis:
assume A47: i in Seg k1 ; :: thesis:
k1 + 1 = len D ;
then k1 <= len D by NAT_1:11;
then Seg k1 c= Seg (len D) by FINSEQ_1:7;
then i in Seg (len D) by A47;
then A48: i in dom D by FINSEQ_1:def 3;
A49: i + 1 in dom D

proof

( 1 <= i & i <= k1 ) by A47, FINSEQ_1:3;
then ( 1 + 0 <= i + 1 & i + 1 <= k1 + 1 ) by XREAL_1:9;
then i + 1 in Seg (len D) by FINSEQ_1:3;
hence i + 1 in dom D by FINSEQ_1:def 3; :: thesis:

end;

A50: (i + 1) - 1 = i ;

now

per cases ;

suppose A51: i = 1 ; :: thesis:

then sup (divset D,i) = D . i by A48, INTEGRA1:def 5;
hence sup (divset D,i) = inf (divset D,(i + 1)) by A49, A50, A51, INTEGRA1:def 5; :: thesis:

end;

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

i >= 1 by A47, FINSEQ_1:3;
then i + 1 >= 1 + 1 by XREAL_1:8;
then A53: i + 1 <> 1 ;
sup (divset D,i) = D . i by A48, A52, INTEGRA1:def 5;
hence sup (divset D,i) = inf (divset D,(i + 1)) by A49, A50, A53, INTEGRA1:def 5; :: thesis:

end;

hence sup (divset D,i) = inf (divset D,(i + 1)) ; :: thesis:

end;

A54: s1 = s2

proof

X: dom s1 = Seg k1 by A42, FINSEQ_1:def 3;
for i being Nat st i in dom s1 holds
s1 . i = s2 . i

proof

let i be Nat; :: thesis:
assume A55: i in dom s1 ; :: thesis:
then s1 . i = f . (sup (divset D,i)) by A42;
then s1 . i = f . (inf (divset D,(i + 1))) by A46, A55, X;
hence s1 . i = s2 . i by A44, A55, A43, A45; :: thesis:

end;

hence s1 = s2 by A42, A44, FINSEQ_2:10; :: thesis:

end;

A56: ( len (s1 ^ <*(f . (sup A))*>) = len (<*(f . (inf A))*> ^ s2) & len (s1 ^ <*(f . (sup A))*>) = len p & ( for i being Element of NAT st i in dom (s1 ^ <*(f . (sup A))*>) holds
p . i = ((s1 ^ <*(f . (sup A))*>) /. i) - ((<*(f . (inf A))*> ^ s2) /. i) ) )

proof

dom <*(f . (sup A))*> = Seg 1 by FINSEQ_1:def 8;
then A57: len <*(f . (sup A))*> = 1 by FINSEQ_1:def 3;
dom <*(f . (inf A))*> = Seg 1 by FINSEQ_1:def 8;
then A58: len <*(f . (inf A))*> = 1 by FINSEQ_1:def 3;
A59: len (s1 ^ <*(f . (sup A))*>) = k1 + 1 by A42, A57, FINSEQ_1:35;
hence A60: len (s1 ^ <*(f . (sup A))*>) = len (<*(f . (inf A))*> ^ s2) by A44, A58, FINSEQ_1:35; :: thesis:
thus len (s1 ^ <*(f . (sup A))*>) = len p by A39, A59; :: thesis:
let i be Element of NAT ; :: thesis:
assume A61: i in dom (s1 ^ <*(f . (sup A))*>) ; :: thesis:
A62: i in dom (<*(f . (inf A))*> ^ s2)

proof

i in Seg (len (s1 ^ <*(f . (sup A))*>)) by A61, FINSEQ_1:def 3;
hence i in dom (<*(f . (inf A))*> ^ s2) by A60, FINSEQ_1:def 3; :: thesis:

end;

A63: ( len D = 1 or len D >= 2 )

proof

( len D = 1 or not len D is trivial ) by NAT_2:def 1;
hence ( len D = 1 or len D >= 2 ) by NAT_2:31; :: thesis:

end;

A64: (s1 ^ <*(f . (sup A))*>) /. i = (s1 ^ <*(f . (sup A))*>) . i by A61, PARTFUN1:def 8;
A65: (<*(f . (inf A))*> ^ s2) /. i = (<*(f . (inf A))*> ^ s2) . i by A62, PARTFUN1:def 8;

now

per cases by A63;

suppose A66: len D = 1 ; :: thesis:

then A67: i in Seg 1 by A59, A61, FINSEQ_1:def 3;
then A68: i = 1 by FINSEQ_1:4, TARSKI:def 1;
A69: ( i in Seg (len D) & i in dom D ) by A66, A67, FINSEQ_1:def 3;
s1 = {} by A42, A66;
then s1 ^ <*(f . (sup A))*> = <*(f . (sup A))*> by FINSEQ_1:47;
then A70: (s1 ^ <*(f . (sup A))*>) /. i = f . (sup A) by A64, A68, FINSEQ_1:def 8;
s2 = {} by A44, A66;
then <*(f . (inf A))*> ^ s2 = <*(f . (inf A))*> by FINSEQ_1:47;
then A71: (<*(f . (inf A))*> ^ s2) /. i = f . (inf A) by A65, A68, FINSEQ_1:def 8;
D . i = sup A by A66, A68, INTEGRA1:def 2;
then A72: sup (divset D,i) = sup A by A68, A69, INTEGRA1:def 5;
p . i = (f . (sup (divset D,i))) - (f . (inf (divset D,i))) by A39, A66, A67, A40;
hence p . i = ((s1 ^ <*(f . (sup A))*>) /. i) - ((<*(f . (inf A))*> ^ s2) /. i) by A68, A69, A70, A71, A72, INTEGRA1:def 5; :: thesis:

end;

suppose A73: len D >= 2 ; :: thesis:

A74: k1 >= 1

proof

1 = 2 - 1 ;
hence k1 >= 1 by A73, XREAL_1:11; :: thesis:

end;

now

per cases ;

suppose A75: i = 1 ; :: thesis:

A76: ( i in Seg (len D) & i in dom D )

proof

A77: Seg 2 c= Seg (len D) by A73, FINSEQ_1:7;
i in Seg 2 by A75, FINSEQ_1:4, TARSKI:def 2;
hence i in Seg (len D) by A77; :: thesis:
hence i in dom D by FINSEQ_1:def 3; :: thesis:

end;

A78: ( i in Seg 1 & i in Seg k1 & i in dom s1 )

proof

A79: Seg 1 c= Seg k1 by A74, FINSEQ_1:7;
thus i in Seg 1 by A75, FINSEQ_1:4, TARSKI:def 1; :: thesis:
hence i in Seg k1 by A79; :: thesis:
hence i in dom s1 by A42, FINSEQ_1:def 3; :: thesis:

end;

then (s1 ^ <*(f . (sup A))*>) . i = s1 . i by FINSEQ_1:def 7;
then A80: (s1 ^ <*(f . (sup A))*>) . i = f . (sup (divset D,i)) by A42, A78;
A81: (<*(f . (inf A))*> ^ s2) . i = f . (inf A)

proof

i in dom <*(f . (inf A))*> by A78, FINSEQ_1:def 8;
then (<*(f . (inf A))*> ^ s2) . i = <*(f . (inf A))*> . i by FINSEQ_1:def 7;
hence (<*(f . (inf A))*> ^ s2) . i = f . (inf A) by A75, FINSEQ_1:def 8; :: thesis:

end;

p . i = (f . (sup (divset D,i))) - (f . (inf (divset D,i))) by A39, A76, A40;
hence p . i = ((s1 ^ <*(f . (sup A))*>) /. i) - ((<*(f . (inf A))*> ^ s2) /. i) by A64, A65, A75, A76, A80, A81, INTEGRA1:def 5; :: thesis:

end;

suppose A82: i = len D ; :: thesis:

A83: ( i in Seg (len D) & i in dom D )

proof

thus i in Seg (len D) by A82, FINSEQ_1:5; :: thesis:
hence i in dom D by FINSEQ_1:def 3; :: thesis:

end;

A84: ( i - (len s1) = 1 & i - (len s1) in dom <*(f . (sup A))*> & i = (i - (len s1)) + (len s1) & i <> 1 )

proof

thus i - (len s1) = 1 by A42, A82; :: thesis:
i - (len s1) in Seg 1 by A42, A82, FINSEQ_1:4, TARSKI:def 1;
hence i - (len s1) in dom <*(f . (sup A))*> by FINSEQ_1:def 8; :: thesis:
thus i = (i - (len s1)) + (len s1) ; :: thesis:
thus i <> 1 by A73, A82; :: thesis:

end;

then (s1 ^ <*(f . (sup A))*>) . i = <*(f . (sup A))*> . (i - (len s1)) by FINSEQ_1:def 7;
then A85: (s1 ^ <*(f . (sup A))*>) /. i = f . (sup A) by A64, A84, FINSEQ_1:def 8;
A86: ( i - (len <*(f . (inf A))*>) = i - 1 & (len <*(f . (inf A))*>) + (i - (len <*(f . (inf A))*>)) = i & i - 1 in Seg k1 & i - (len <*(f . (inf A))*>) in dom s2 & (i - 1) + 1 = i )

proof

thus A87: i - (len <*(f . (inf A))*>) = i - 1 by FINSEQ_1:57; :: thesis:
thus (len <*(f . (inf A))*>) + (i - (len <*(f . (inf A))*>)) = i ; :: thesis:
( i - 1 <> 0 & i - 1 = k1 ) by A73, A82;
hence i - 1 in Seg k1 by FINSEQ_1:5; :: thesis:
hence i - (len <*(f . (inf A))*>) in dom s2 by A44, A87, FINSEQ_1:def 3; :: thesis:
thus (i - 1) + 1 = i ; :: thesis:

end;

A89: (<*(f . (inf A))*> ^ s2) . i = f . (D . (i - 1))

proof

(<*(f . (inf A))*> ^ s2) . i = s2 . (i - (len <*(f . (inf A))*>)) by A86, FINSEQ_1:def 7;
then (<*(f . (inf A))*> ^ s2) . i = f . (inf (divset D,i)) by A44, A86;
hence (<*(f . (inf A))*> ^ s2) . i = f . (D . (i - 1)) by A83, A84, INTEGRA1:def 5; :: thesis:

end;

p . i = (f . (sup (divset D,i))) - (f . (inf (divset D,i))) by A39, A83, A40;
then p . i = (f . (sup (divset D,i))) - (f . (D . (i - 1))) by A83, A84, INTEGRA1:def 5;
then p . i = (f . (D . i)) - (f . (D . (i - 1))) by A83, A84, INTEGRA1:def 5;
hence p . i = ((s1 ^ <*(f . (sup A))*>) /. i) - ((<*(f . (inf A))*> ^ s2) /. i) by A65, A82, A85, A89, INTEGRA1:def 2; :: thesis:

end;

suppose A90: ( i <> 1 & i <> len D ) ; :: thesis:

A91: ( i in Seg (len D) & i in dom D )

proof

A92: (len s1) + (len <*(f . (sup A))*>) = k1 + 1 by A42, FINSEQ_1:56;
hence i in Seg (len D) by A61, FINSEQ_1:def 7; :: thesis:
dom (s1 ^ <*(f . (sup A))*>) = Seg (len D) by A92, FINSEQ_1:def 7;
hence i in dom D by A61, FINSEQ_1:def 3; :: thesis:

end;

A93: ( i in dom s1 & i in Seg k1 & i - 1 in Seg k1 & (i - 1) + 1 = i & i - (len <*(f . (inf A))*>) in dom s2 )

proof

A94: ( 1 <= i & i <= len D ) by A91, FINSEQ_1:3;
then A95: ( 1 <= i & i < k1 + 1 ) by A90, XXREAL_0:1;
then A96: ( 1 <= i & i <= k1 ) by NAT_1:13;
then i in Seg (len s1) by A42, FINSEQ_1:3;
hence i in dom s1 by FINSEQ_1:def 3; :: thesis:
thus i in Seg k1 by A96, FINSEQ_1:3; :: thesis:
consider j being Nat such that
A97: i = 1 + j by A94, NAT_1:10;
( i <> 0 & i <> 1 ) by A90, A91, FINSEQ_1:3;
then not i is trivial by NAT_2:def 1;
then ( i >= 2 & i <= k1 ) by A95, NAT_1:13, NAT_2:31;
then ( i >= 1 + 1 & i - 1 <= k1 - 1 ) by XREAL_1:11;
then ( i - 1 >= 1 & (i - 1) + 0 <= (k1 - 1) + 1 ) by XREAL_1:9, XREAL_1:21;
hence i - 1 in Seg k1 by A97, FINSEQ_1:3; :: thesis:
then A98: i - (len <*(f . (inf A))*>) in Seg (len s2) by A44, FINSEQ_1:56;
thus (i - 1) + 1 = i ; :: thesis:
thus i - (len <*(f . (inf A))*>) in dom s2 by A98, FINSEQ_1:def 3; :: thesis:

end;

A99: (s1 ^ <*(f . (sup A))*>) . i = f . (D . i)

proof

(s1 ^ <*(f . (sup A))*>) . i = s1 . i by A93, FINSEQ_1:def 7;
then (s1 ^ <*(f . (sup A))*>) . i = f . (sup (divset D,i)) by A42, A93;
hence (s1 ^ <*(f . (sup A))*>) . i = f . (D . i) by A90, A91, INTEGRA1:def 5; :: thesis:

end;

A100: (<*(f . (inf A))*> ^ s2) . i = f . (D . (i - 1))

proof

A101: i - (len <*(f . (inf A))*>) in Seg (len s2) by A93, FINSEQ_1:def 3;
( 1 <= i - (len <*(f . (inf A))*>) & i - (len <*(f . (inf A))*>) <= len s2 ) by A101, FINSEQ_1:3;
then ( (len <*(f . (inf A))*>) + 1 <= i & i <= (len <*(f . (inf A))*>) + (len s2) ) by XREAL_1:21, XREAL_1:22;
then (<*(f . (inf A))*> ^ s2) . i = s2 . (i - (len <*(f . (inf A))*>)) by FINSEQ_1:36;
then (<*(f . (inf A))*> ^ s2) . i = s2 . (i - 1) by FINSEQ_1:56;
then (<*(f . (inf A))*> ^ s2) . i = f . (inf (divset D,i)) by A44, A93, A45;
hence (<*(f . (inf A))*> ^ s2) . i = f . (D . (i - 1)) by A90, A91, INTEGRA1:def 5; :: thesis:

end;

p . i = (f . (sup (divset D,i))) - (f . (inf (divset D,i))) by A39, A91, A40;
then p . i = (f . (sup (divset D,i))) - (f . (D . (i - 1))) by A90, A91, INTEGRA1:def 5;
hence p . i = ((s1 ^ <*(f . (sup A))*>) /. i) - ((<*(f . (inf A))*> ^ s2) /. i) by A64, A65, A90, A91, A99, A100, INTEGRA1:def 5; :: thesis:

end;

hence p . i = ((s1 ^ <*(f . (sup A))*>) /. i) - ((<*(f . (inf A))*> ^ s2) /. i) ; :: thesis:

end;

hence p . i = ((s1 ^ <*(f . (sup A))*>) /. i) - ((<*(f . (inf A))*> ^ s2) /. i) ; :: thesis:

end;

A103: Sum p = (((Sum s1) + (f . (sup A))) - (f . (inf A))) - (Sum s2)

proof

Sum p = (Sum (s1 ^ <*(f . (sup A))*>)) - (Sum (<*(f . (inf A))*> ^ s2)) by A56, INTEGRA1:24;
then Sum p = ((Sum s1) + (f . (sup A))) - (Sum (<*(f . (inf A))*> ^ s2)) by RVSUM_1:104;
then Sum p = ((Sum s1) + (f . (sup A))) - ((f . (inf A)) + (Sum s2)) by RVSUM_1:106;
hence Sum p = (((Sum s1) + (f . (sup A))) - (f . (inf A))) - (Sum s2) ; :: thesis:

end;

A104: lower_sum ((f `| X) || A),D <= (f . (sup A)) - (f . (inf A))

proof

A105: for k being Element of NAT st k in dom D holds
(f . (sup (divset D,k))) - (f . (inf (divset D,k))) >= (lower_volume ((f `| X) || A),D) . k

proof

let k be Element of NAT ; :: thesis:
assume A106: k in dom D ; :: thesis:
then consider r being Real such that
A107: ( r in divset D,k & (f . (sup (divset D,k))) - (f . (inf (divset D,k))) = (diff f,r) * (vol (divset D,k)) ) by A4;
A108: diff f,r in rng (((f `| X) || A) | (divset D,k)) by A21, A106, A107;
rng (((f `| X) || A) | (divset D,k)) is bounded by A29, A106;
then ( rng (((f `| X) || A) | (divset D,k)) is bounded_above & rng (((f `| X) || A) | (divset D,k)) is bounded_below ) ;
then A109: diff f,r >= inf (rng (((f `| X) || A) | (divset D,k))) by A108, SEQ_4:def 5;
A110: vol (divset D,k) >= 0 by INTEGRA1:11;
k in Seg (len D) by A106, FINSEQ_1:def 3;
then k in dom D by FINSEQ_1:def 3;
then (inf (rng (((f `| X) || A) | (divset D,k)))) * (vol (divset D,k)) = (lower_volume ((f `| X) || A),D) . k by INTEGRA1:def 8;
hence (f . (sup (divset D,k))) - (f . (inf (divset D,k))) >= (lower_volume ((f `| X) || A),D) . k by A107, A109, A110, XREAL_1:66; :: thesis:

end;

(f . (sup A)) - (f . (inf A)) >= lower_sum ((f `| X) || A),D

proof

A111: for k being Nat st k in Seg (len D) holds
p . k >= (lower_volume ((f `| X) || A),D) . k

proof

let k be Nat; :: thesis:
assume A112: k in Seg (len D) ; :: thesis:
then A113: (f . (sup (divset D,k))) - (f . (inf (divset D,k))) = p . k by A39, A40;
k in dom D by A112, FINSEQ_1:def 3;
hence p . k >= (lower_volume ((f `| X) || A),D) . k by A105, A113; :: thesis:

end;

reconsider p = p as Element of (len D) -tuples_on REAL by A39, FINSEQ_2:110;
len (lower_volume ((f `| X) || A),D) = len D by INTEGRA1:def 8;
then reconsider q = lower_volume ((f `| X) || A),D as Element of (len D) -tuples_on REAL by FINSEQ_2:110;
Sum q <= Sum p by A111, RVSUM_1:112;
hence (f . (sup A)) - (f . (inf A)) >= lower_sum ((f `| X) || A),D by A54, A103, INTEGRA1:def 10; :: thesis:

end;

hence lower_sum ((f `| X) || A),D <= (f . (sup A)) - (f . (inf A)) ; :: thesis:

end;

(f . (sup A)) - (f . (inf A)) <= upper_sum ((f `| X) || A),D

proof

A114: for k being Element of NAT st k in dom D holds
(f . (sup (divset D,k))) - (f . (inf (divset D,k))) <= (upper_volume ((f `| X) || A),D) . k

proof

let k be Element of NAT ; :: thesis:
assume A115: k in dom D ; :: thesis:
then consider r being Real such that
A116: ( r in divset D,k & (f . (sup (divset D,k))) - (f . (inf (divset D,k))) = (diff f,r) * (vol (divset D,k)) ) by A4;
A117: diff f,r in rng (((f `| X) || A) | (divset D,k)) by A21, A115, A116;
rng (((f `| X) || A) | (divset D,k)) is bounded by A29, A115;
then ( rng (((f `| X) || A) | (divset D,k)) is bounded_above & rng (((f `| X) || A) | (divset D,k)) is bounded_below ) ;
then A118: diff f,r <= sup (rng (((f `| X) || A) | (divset D,k))) by A117, SEQ_4:def 4;
vol (divset D,k) >= 0 by INTEGRA1:11;
then A119: (diff f,r) * (vol (divset D,k)) <= (sup (rng (((f `| X) || A) | (divset D,k)))) * (vol (divset D,k)) by A118, XREAL_1:66;
k in Seg (len D) by A115, FINSEQ_1:def 3;
then k in dom D by FINSEQ_1:def 3;
hence (f . (sup (divset D,k))) - (f . (inf (divset D,k))) <= (upper_volume ((f `| X) || A),D) . k by A116, A119, INTEGRA1:def 7; :: thesis:

end;

(f . (sup A)) - (f . (inf A)) <= upper_sum ((f `| X) || A),D

proof

A120: for k being Nat st k in Seg (len D) holds
p . k <= (upper_volume ((f `| X) || A),D) . k

proof

let k be Nat; :: thesis:
assume A121: k in Seg (len D) ; :: thesis:
then A122: (f . (sup (divset D,k))) - (f . (inf (divset D,k))) = p . k by A39, A40;
k in dom D by A121, FINSEQ_1:def 3;
hence p . k <= (upper_volume ((f `| X) || A),D) . k by A114, A122; :: thesis:

end;

reconsider p = p as Element of (len D) -tuples_on REAL by A39, FINSEQ_2:110;
len (upper_volume ((f `| X) || A),D) = len D by INTEGRA1:def 7;
then reconsider q = upper_volume ((f `| X) || A),D as Element of (len D) -tuples_on REAL by FINSEQ_2:110;
Sum p <= Sum q by A120, RVSUM_1:112;
hence (f . (sup A)) - (f . (inf A)) <= upper_sum ((f `| X) || A),D by A54, A103, INTEGRA1:def 9; :: thesis:

end;

hence (f . (sup A)) - (f . (inf A)) <= upper_sum ((f `| X) || A),D ; :: thesis:

end;

hence ( lower_sum ((f `| X) || A),D <= (f . (sup A)) - (f . (inf A)) & (f . (sup A)) - (f . (inf A)) <= upper_sum ((f `| X) || A),D ) by A104; :: thesis: