let x be Real; :: thesis:
let A be non empty closed_interval Subset of REAL; :: thesis:
let D1, D2 be Division of A; :: thesis:
let f be Function of A,REAL; :: thesis:
assume that
A1: x in divset (D1,(len D1)) and
A2: vol A <> 0 and
A3: D1 <= D2 and
A4: rng D2 = (rng D1) \/ {x} and
A5: f | A is bounded and
A6: x > lower_bound A ; :: thesis:
len D1 in Seg (len D1) by FINSEQ_1:3;
then A7: 1 <= len D1 by FINSEQ_1:1;
then ( len D1 = 1 or len D1 > 1 ) by XXREAL_0:1;
then A8: ( len D1 = 1 or len D1 >= 1 + 1 ) by NAT_1:13;

now

per cases by A8;

suppose A9: len D1 = 1 ; :: thesis:

then reconsider MD1 = <*(lower_bound A)*> ^ D1 as non empty increasing FinSequence of REAL by A2, Lm8;
A10: len MD1 = (len <*(lower_bound A)*>) + (len D1) by FINSEQ_1:22;
(len <*(lower_bound A)*>) + 1 <= (len <*(lower_bound A)*>) + (len D1) by A7, XREAL_1:6;
then MD1 . (len MD1) = D1 . (((len <*(lower_bound A)*>) + (len D1)) - (len <*(lower_bound A)*>)) by A10, FINSEQ_1:23
.= D1 . (len D1) ;
then A11: MD1 . (len MD1) = upper_bound A by INTEGRA1:def 2;
for y being Real st y in rng MD1 holds
y in A

proof

let y be Real; :: thesis:
assume y in rng MD1 ; :: thesis:
then A12: y in (rng <*(lower_bound A)*>) \/ (rng D1) by FINSEQ_1:31;

per cases by A12, XBOOLE_0:def 3;

suppose y in rng <*(lower_bound A)*> ; :: thesis:

then y in {(lower_bound A)} by FINSEQ_1:38;
then A13: y = lower_bound A by TARSKI:def 1;
ex a, b being Real st
( a <= b & a = lower_bound A & b = upper_bound A ) by SEQ_4:11;
hence y in A by A13, INTEGRA2:1; :: thesis:

end;

suppose A14: y in rng D1 ; :: thesis:

rng D1 c= A by INTEGRA1:def 2;
hence y in A by A14; :: thesis:

end;

end;

end;

then rng MD1 c= A by SUBSET_1:2;
then reconsider MD1 = MD1 as Division of A by A11, INTEGRA1:def 2;
A15: len MD1 = (len <*(lower_bound A)*>) + (len D1) by FINSEQ_1:22
.= 1 + (len D1) by FINSEQ_1:39 ;
A16: vol A >= 0 by INTEGRA1:9;
D1 . 1 = upper_bound A by A9, INTEGRA1:def 2;
then (D1 . 1) - (lower_bound A) > 0 by A2, A16, INTEGRA1:def 5;
then A17: lower_bound A < D1 . 1 by XREAL_1:47;
upper_volume (f,D1) = (upper_volume (f,MD1)) /^ 1 by Lm10;
then upper_volume (f,MD1) = <*((upper_volume (f,MD1)) /. 1)*> ^ (upper_volume (f,D1)) by FINSEQ_5:29;
then A18: Sum (upper_volume (f,MD1)) = ((upper_volume (f,MD1)) /. 1) + (Sum (upper_volume (f,D1))) by RVSUM_1:76;
A19: len D1 in dom D1 by FINSEQ_5:6;
A20: 1 + (len D1) >= 1 + 1 by A7, XREAL_1:6;
then A21: len MD1 <> 1 by A15;
A22: len MD1 in dom MD1 by FINSEQ_5:6;
(len MD1) - 1 = len D1 by A15;
then lower_bound (divset (MD1,(len MD1))) = MD1 . (len D1) by A22, A21, INTEGRA1:def 4
.= lower_bound A by A9, FINSEQ_1:41 ;
then A23: lower_bound (divset (D1,(len D1))) = lower_bound (divset (MD1,(len MD1))) by A9, A19, INTEGRA1:def 4;
set MD2 = <*(lower_bound A)*> ^ D2;
rng MD1 <> {} ;
then A24: 1 in dom MD1 by FINSEQ_3:32;
then A25: (upper_volume (f,MD1)) . 1 = (upper_bound (rng (f | (divset (MD1,1))))) * (vol (divset (MD1,1))) by INTEGRA1:def 6;
1 in Seg (len MD1) by A24, FINSEQ_1:def 3;
then 1 in Seg (len (upper_volume (f,MD1))) by INTEGRA1:def 6;
then A26: 1 in dom (upper_volume (f,MD1)) by FINSEQ_1:def 3;
rng D2 <> {} ;
then A27: 1 in dom D2 by FINSEQ_3:32;
then 1 <= len D2 by FINSEQ_3:25;
then A28: (len <*(lower_bound A)*>) + 1 <= (len <*(lower_bound A)*>) + (len D2) by XREAL_1:6;
A29: D2 . 1 in rng D2 by A27, FUNCT_1:def 3;
lower_bound A < D2 . 1

proof

per cases by A4, A29, XBOOLE_0:def 3;

suppose A30: D2 . 1 in rng D1 ; :: thesis:

rng D1 <> {} ;
then A31: 1 in dom D1 by FINSEQ_3:32;
consider k being Element of NAT such that
A32: k in dom D1 and
A33: D1 . k = D2 . 1 by A30, PARTFUN1:3;
1 <= k by A32, FINSEQ_3:25;
then D1 . 1 <= D2 . 1 by A32, A33, A31, SEQ_4:137;
hence lower_bound A < D2 . 1 by A17, XXREAL_0:2; :: thesis:

end;

suppose D2 . 1 in {x} ; :: thesis:

hence lower_bound A < D2 . 1 by A6, TARSKI:def 1; :: thesis:

end;

end;

end;

then reconsider MD2 = <*(lower_bound A)*> ^ D2 as non empty increasing FinSequence of REAL by Lm9;
len MD2 = (len <*(lower_bound A)*>) + (len D2) by FINSEQ_1:22;
then MD2 . (len MD2) = D2 . (((len <*(lower_bound A)*>) + (len D2)) - (len <*(lower_bound A)*>)) by A28, FINSEQ_1:23
.= D2 . (len D2) ;
then A34: MD2 . (len MD2) = upper_bound A by INTEGRA1:def 2;
for y being Real st y in rng MD2 holds
y in A

proof

let y be Real; :: thesis:
assume y in rng MD2 ; :: thesis:
then A35: y in (rng <*(lower_bound A)*>) \/ (rng D2) by FINSEQ_1:31;

per cases by A35, XBOOLE_0:def 3;

suppose y in rng <*(lower_bound A)*> ; :: thesis:

then y in {(lower_bound A)} by FINSEQ_1:38;
then A36: y = lower_bound A by TARSKI:def 1;
ex a, b being Real st
( a <= b & a = lower_bound A & b = upper_bound A ) by SEQ_4:11;
hence y in A by A36, INTEGRA2:1; :: thesis:

end;

suppose A37: y in rng D2 ; :: thesis:

rng D2 c= A by INTEGRA1:def 2;
hence y in A by A37; :: thesis:

end;

end;

end;

then rng MD2 c= A by SUBSET_1:2;
then reconsider MD2 = MD2 as Division of A by A34, INTEGRA1:def 2;
A38: x <= upper_bound (divset (D1,(len D1))) by A1, INTEGRA2:1;
rng MD2 = (rng D2) \/ (rng <*(lower_bound A)*>) by FINSEQ_1:31
.= ((rng D1) \/ (rng <*(lower_bound A)*>)) \/ {x} by A4, XBOOLE_1:4 ;
then A39: rng MD2 = (rng MD1) \/ {x} by FINSEQ_1:31;
MD1 . (len MD1) = MD1 . ((len <*(lower_bound A)*>) + (len D1)) by FINSEQ_1:22
.= D1 . (len D1) by A19, FINSEQ_1:def 7 ;
then A40: upper_bound (divset (MD1,(len MD1))) = D1 . (len D1) by A22, A21, INTEGRA1:def 4
.= upper_bound (divset (D1,(len D1))) by A9, A19, INTEGRA1:def 4 ;
rng D1 c= rng D2 by A3, INTEGRA1:def 18;
then (rng D1) \/ (rng <*(lower_bound A)*>) c= (rng D2) \/ (rng <*(lower_bound A)*>) by XBOOLE_1:9;
then rng MD1 c= (rng D2) \/ (rng <*(lower_bound A)*>) by FINSEQ_1:31;
then A41: rng MD1 c= rng MD2 by FINSEQ_1:31;
len D1 <= len D2 by A3, INTEGRA1:def 18;
then (len D1) + (len <*(lower_bound A)*>) <= (len D2) + (len <*(lower_bound A)*>) by XREAL_1:6;
then len MD1 <= (len D2) + (len <*(lower_bound A)*>) by FINSEQ_1:22;
then len MD1 <= len MD2 by FINSEQ_1:22;
then A42: MD1 <= MD2 by A41, INTEGRA1:def 18;
lower_bound (divset (D1,(len D1))) <= x by A1, INTEGRA2:1;
then x in divset (MD1,(len MD1)) by A38, A23, A40, INTEGRA2:1;
then A43: (Sum (upper_volume (f,MD1))) - (Sum (upper_volume (f,MD2))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta MD1) by A5, A15, A20, A42, A39, Th11;
rng MD2 <> {} ;
then A44: 1 in dom MD2 by FINSEQ_3:32;
then A45: (upper_volume (f,MD2)) . 1 = (upper_bound (rng (f | (divset (MD2,1))))) * (vol (divset (MD2,1))) by INTEGRA1:def 6;
1 in Seg (len MD2) by A44, FINSEQ_1:def 3;
then 1 in Seg (len (upper_volume (f,MD2))) by INTEGRA1:def 6;
then A46: 1 in dom (upper_volume (f,MD2)) by FINSEQ_1:def 3;
vol (divset (MD2,1)) = 0 by Lm11;
then A47: (upper_volume (f,MD2)) /. 1 = 0 by A45, A46, PARTFUN1:def 6;
upper_volume (f,D2) = (upper_volume (f,MD2)) /^ 1 by Lm10;
then upper_volume (f,MD2) = <*((upper_volume (f,MD2)) /. 1)*> ^ (upper_volume (f,D2)) by FINSEQ_5:29;
then A48: Sum (upper_volume (f,MD2)) = ((upper_volume (f,MD2)) /. 1) + (Sum (upper_volume (f,D2))) by RVSUM_1:76;
vol (divset (MD1,1)) = 0 by Lm11;
then (upper_volume (f,MD1)) /. 1 = 0 by A25, A26, PARTFUN1:def 6;
hence (Sum (upper_volume (f,D1))) - (Sum (upper_volume (f,D2))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1) by A43, A18, A48, A47, Lm12; :: thesis:

end;

suppose len D1 >= 2 ; :: thesis:

hence (Sum (upper_volume (f,D1))) - (Sum (upper_volume (f,D2))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1) by A1, A3, A4, A5, Th11; :: thesis:

end;

end;

end;

hence (Sum (upper_volume (f,D1))) - (Sum (upper_volume (f,D2))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1) ; :: thesis: