let x be Real; :: thesis:
let A be 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:5;
then A7: 1 <= len D1 by FINSEQ_1:3;
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 A10: D1 . 1 = upper_bound A by INTEGRA1:def 2;
vol A >= 0 by INTEGRA1:11;
then (D1 . 1) - (lower_bound A) > 0 by A2, A10, INTEGRA1:def 6;
then A11: lower_bound A < D1 . 1 by XREAL_1:49;
reconsider MD1 = <*(lower_bound A)*> ^ D1 as non empty increasing FinSequence of REAL by A2, A9, Lm9;
MD1 is Division of A

proof

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

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:55;
then A13: y = lower_bound A by TARSKI:def 1;
consider a, b being Real such that
A14: ( a <= b & a = lower_bound A & b = upper_bound A ) by INTEGRA1:4;
thus y in A by A13, A14, INTEGRA2:1; :: thesis:

end;

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

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

end;

then A16: rng MD1 c= A by SUBSET_1:7;
MD1 . (len MD1) = upper_bound A

proof

A17: len MD1 = (len <*(lower_bound A)*>) + (len D1) by FINSEQ_1:35;
(len <*(lower_bound A)*>) + 1 <= (len <*(lower_bound A)*>) + (len D1) by A7, XREAL_1:8;
then MD1 . (len MD1) = D1 . (((len <*(lower_bound A)*>) + (len D1)) - (len <*(lower_bound A)*>)) by A17, FINSEQ_1:36
.= D1 . (len D1) ;
hence MD1 . (len MD1) = upper_bound A by INTEGRA1:def 2; :: thesis:

end;

hence MD1 is Division of A by A16, INTEGRA1:def 2; :: thesis:

end;

then reconsider MD1 = MD1 as Division of A by INTEGRA1:def 2;
rng D2 <> {} ;
then A18: 1 in dom D2 by FINSEQ_3:34;
then A19: 1 <= len D2 by FINSEQ_3:27;
A20: D2 . 1 in rng D2 by A18, FUNCT_1:def 5;
A21: lower_bound A < D2 . 1

proof

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

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

then consider k being Element of NAT such that
A22: ( k in dom D1 & D1 . k = D2 . 1 ) by PARTFUN1:26;
A23: ( 1 <= k & k <= len D1 ) by A22, FINSEQ_3:27;
rng D1 <> {} ;
then 1 in dom D1 by FINSEQ_3:34;
then D1 . 1 <= D2 . 1 by A22, A23, GOBOARD2:18;
hence lower_bound A < D2 . 1 by A11, XXREAL_0:2; :: thesis:

end;

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

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

end;

set MD2 = <*(lower_bound A)*> ^ D2;
reconsider MD2 = <*(lower_bound A)*> ^ D2 as non empty increasing FinSequence of REAL by A21, Lm10;
MD2 is Division of A

proof

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 A24: y in (rng <*(lower_bound A)*>) \/ (rng D2) by FINSEQ_1:44;

per cases by A24, XBOOLE_0:def 3;

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

then y in {(lower_bound A)} by FINSEQ_1:55;
then A25: y = lower_bound A by TARSKI:def 1;
consider a, b being Real such that
A26: ( a <= b & a = lower_bound A & b = upper_bound A ) by INTEGRA1:4;
thus y in A by A25, A26, INTEGRA2:1; :: thesis:

end;

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

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

end;

then A28: rng MD2 c= A by SUBSET_1:7;
MD2 . (len MD2) = upper_bound A

proof

A29: len MD2 = (len <*(lower_bound A)*>) + (len D2) by FINSEQ_1:35;
(len <*(lower_bound A)*>) + 1 <= (len <*(lower_bound A)*>) + (len D2) by A19, XREAL_1:8;
then MD2 . (len MD2) = D2 . (((len <*(lower_bound A)*>) + (len D2)) - (len <*(lower_bound A)*>)) by A29, FINSEQ_1:36
.= D2 . (len D2) ;
hence MD2 . (len MD2) = upper_bound A by INTEGRA1:def 2; :: thesis:

end;

hence MD2 is Division of A by A28, INTEGRA1:def 2; :: thesis:

end;

then reconsider MD2 = MD2 as Division of A by INTEGRA1:def 2;
A30: len MD1 = (len <*(lower_bound A)*>) + (len D1) by FINSEQ_1:35
.= 1 + (len D1) by FINSEQ_1:56 ;
A31: 1 + (len D1) >= 1 + 1 by A7, XREAL_1:8;
A32: x in divset MD1,(len MD1)

proof

A33: ( lower_bound (divset D1,(len D1)) <= x & x <= upper_bound (divset D1,(len D1)) ) by A1, INTEGRA2:1;
A34: len D1 in dom D1 by FINSEQ_5:6;
A35: len MD1 in dom MD1 by FINSEQ_5:6;
A36: len MD1 <> 1 by A30, A31;
(len MD1) - 1 = len D1 by A30;
then lower_bound (divset MD1,(len MD1)) = MD1 . (len D1) by A35, A36, INTEGRA1:def 5
.= lower_bound A by A9, FINSEQ_1:58 ;
then A37: lower_bound (divset D1,(len D1)) = lower_bound (divset MD1,(len MD1)) by A9, A34, INTEGRA1:def 5;
MD1 . (len MD1) = MD1 . ((len <*(lower_bound A)*>) + (len D1)) by FINSEQ_1:35
.= D1 . (len D1) by A34, FINSEQ_1:def 7 ;
then upper_bound (divset MD1,(len MD1)) = D1 . (len D1) by A35, A36, INTEGRA1:def 5
.= upper_bound (divset D1,(len D1)) by A9, A34, INTEGRA1:def 5 ;
hence x in divset MD1,(len MD1) by A33, A37, INTEGRA2:1; :: thesis:

end;

A38: MD1 <= MD2

proof

A39: ( len D1 <= len D2 & rng D1 c= rng D2 ) by A3, INTEGRA1:def 20;
then (len D1) + (len <*(lower_bound A)*>) <= (len D2) + (len <*(lower_bound A)*>) by XREAL_1:8;
then len MD1 <= (len D2) + (len <*(lower_bound A)*>) by FINSEQ_1:35;
then A40: len MD1 <= len MD2 by FINSEQ_1:35;
(rng D1) \/ (rng <*(lower_bound A)*>) c= (rng D2) \/ (rng <*(lower_bound A)*>) by A39, XBOOLE_1:9;
then rng MD1 c= (rng D2) \/ (rng <*(lower_bound A)*>) by FINSEQ_1:44;
then rng MD1 c= rng MD2 by FINSEQ_1:44;
hence MD1 <= MD2 by A40, INTEGRA1:def 20; :: thesis:

end;

rng MD2 = (rng MD1) \/ {x}

proof

rng MD2 = (rng D2) \/ (rng <*(lower_bound A)*>) by FINSEQ_1:44
.= ((rng D1) \/ (rng <*(lower_bound A)*>)) \/ {x} by A4, XBOOLE_1:4 ;
hence rng MD2 = (rng MD1) \/ {x} by FINSEQ_1:44; :: thesis:

end;

then A41: (Sum (upper_volume f,MD1)) - (Sum (upper_volume f,MD2)) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta MD1) by A5, A30, A31, A32, A38, Th10;
A42: vol (divset MD1,1) = 0 by Lm12;
upper_volume f,D1 = (upper_volume f,MD1) /^ 1 by Lm11;
then upper_volume f,MD1 = <*((upper_volume f,MD1) /. 1)*> ^ (upper_volume f,D1) by FINSEQ_5:32;
then A43: Sum (upper_volume f,MD1) = ((upper_volume f,MD1) /. 1) + (Sum (upper_volume f,D1)) by RVSUM_1:106;
rng MD1 <> {} ;
then 1 in dom MD1 by FINSEQ_3:34;
then A44: 1 in Seg (len MD1) by FINSEQ_1:def 3;
then 1 in dom MD1 by FINSEQ_1:def 3;
then A45: (upper_volume f,MD1) . 1 = (upper_bound (rng (f | (divset MD1,1)))) * (vol (divset MD1,1)) by INTEGRA1:def 7;
1 in Seg (len (upper_volume f,MD1)) by A44, INTEGRA1:def 7;
then 1 in dom (upper_volume f,MD1) by FINSEQ_1:def 3;
then A46: (upper_volume f,MD1) /. 1 = 0 by A42, A45, PARTFUN1:def 8;
A47: vol (divset MD2,1) = 0 by Lm12;
upper_volume f,D2 = (upper_volume f,MD2) /^ 1 by Lm11;
then upper_volume f,MD2 = <*((upper_volume f,MD2) /. 1)*> ^ (upper_volume f,D2) by FINSEQ_5:32;
then A48: Sum (upper_volume f,MD2) = ((upper_volume f,MD2) /. 1) + (Sum (upper_volume f,D2)) by RVSUM_1:106;
rng MD2 <> {} ;
then 1 in dom MD2 by FINSEQ_3:34;
then A49: 1 in Seg (len MD2) by FINSEQ_1:def 3;
then 1 in dom MD2 by FINSEQ_1:def 3;
then A50: (upper_volume f,MD2) . 1 = (upper_bound (rng (f | (divset MD2,1)))) * (vol (divset MD2,1)) by INTEGRA1:def 7;
1 in Seg (len (upper_volume f,MD2)) by A49, INTEGRA1:def 7;
then 1 in dom (upper_volume f,MD2) by FINSEQ_1:def 3;
then (upper_volume f,MD2) /. 1 = 0 by A47, A50, PARTFUN1:def 8;
hence (Sum (upper_volume f,D1)) - (Sum (upper_volume f,D2)) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1) by A41, A43, A46, A48, Lm13; :: 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, Th10; :: thesis:

end;

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