let x be Real; :: thesis: for A being non empty closed_interval Subset of REAL

for D1, D2 being Division of A

for f being Function of A,REAL st x in divset (D1,(len D1)) & vol A <> 0 & D1 <= D2 & rng D2 = (rng D1) \/ {x} & f | A is bounded & x > lower_bound A holds

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

let A be non empty closed_interval Subset of REAL; :: thesis: for D1, D2 being Division of A

for f being Function of A,REAL st x in divset (D1,(len D1)) & vol A <> 0 & D1 <= D2 & rng D2 = (rng D1) \/ {x} & f | A is bounded & x > lower_bound A holds

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

let D1, D2 be Division of A; :: thesis: for f being Function of A,REAL st x in divset (D1,(len D1)) & vol A <> 0 & D1 <= D2 & rng D2 = (rng D1) \/ {x} & f | A is bounded & x > lower_bound A holds

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

let f be Function of A,REAL; :: thesis: ( x in divset (D1,(len D1)) & vol A <> 0 & D1 <= D2 & rng D2 = (rng D1) \/ {x} & f | A is bounded & x > lower_bound A implies (Sum (upper_volume (f,D1))) - (Sum (upper_volume (f,D2))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1) )

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: (Sum (upper_volume (f,D1))) - (Sum (upper_volume (f,D2))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1)

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;

for D1, D2 being Division of A

for f being Function of A,REAL st x in divset (D1,(len D1)) & vol A <> 0 & D1 <= D2 & rng D2 = (rng D1) \/ {x} & f | A is bounded & x > lower_bound A holds

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

let A be non empty closed_interval Subset of REAL; :: thesis: for D1, D2 being Division of A

for f being Function of A,REAL st x in divset (D1,(len D1)) & vol A <> 0 & D1 <= D2 & rng D2 = (rng D1) \/ {x} & f | A is bounded & x > lower_bound A holds

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

let D1, D2 be Division of A; :: thesis: for f being Function of A,REAL st x in divset (D1,(len D1)) & vol A <> 0 & D1 <= D2 & rng D2 = (rng D1) \/ {x} & f | A is bounded & x > lower_bound A holds

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

let f be Function of A,REAL; :: thesis: ( x in divset (D1,(len D1)) & vol A <> 0 & D1 <= D2 & rng D2 = (rng D1) \/ {x} & f | A is bounded & x > lower_bound A implies (Sum (upper_volume (f,D1))) - (Sum (upper_volume (f,D2))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1) )

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: (Sum (upper_volume (f,D1))) - (Sum (upper_volume (f,D2))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1)

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 :: thesis: (Sum (upper_volume (f,D1))) - (Sum (upper_volume (f,D2))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1)end;

hence
(Sum (upper_volume (f,D1))) - (Sum (upper_volume (f,D2))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1)
; :: thesis: verumper cases
( len D1 = 1 or len D1 >= 2 )
by A8;

end;

suppose A9:
len D1 = 1
; :: thesis: (Sum (upper_volume (f,D1))) - (Sum (upper_volume (f,D2))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1)

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 Element of REAL st y in rng MD1 holds

y in A

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

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 Element of REAL st y in rng MD2 holds

y in A

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: verum

end;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 Element of REAL st y in rng MD1 holds

y in A

proof

then
rng MD1 c= A
;
let y be Element of REAL ; :: thesis: ( y in rng MD1 implies y in A )

assume y in rng MD1 ; :: thesis: y in A

then A12: y in (rng <*(lower_bound A)*>) \/ (rng D1) by FINSEQ_1:31;

end;assume y in rng MD1 ; :: thesis: y in A

then A12: y in (rng <*(lower_bound A)*>) \/ (rng D1) by FINSEQ_1:31;

per cases
( y in rng <*(lower_bound A)*> or y in rng D1 )
by A12, XBOOLE_0:def 3;

end;

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

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: verum

end;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: verum

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
end;

then reconsider MD2 = <*(lower_bound A)*> ^ D2 as non empty increasing FinSequence of REAL by Lm9;per cases
( D2 . 1 in rng D1 or D2 . 1 in {x} )
by A4, A29, XBOOLE_0:def 3;

end;

suppose A30:
D2 . 1 in rng D1
; :: thesis: lower_bound A < D2 . 1

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: verum

end;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: verum

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 Element of REAL st y in rng MD2 holds

y in A

proof

then
rng MD2 c= A
;
let y be Element of REAL ; :: thesis: ( y in rng MD2 implies y in A )

assume y in rng MD2 ; :: thesis: y in A

then A35: y in (rng <*(lower_bound A)*>) \/ (rng D2) by FINSEQ_1:31;

end;assume y in rng MD2 ; :: thesis: y in A

then A35: y in (rng <*(lower_bound A)*>) \/ (rng D2) by FINSEQ_1:31;

per cases
( y in rng <*(lower_bound A)*> or y in rng D2 )
by A35, XBOOLE_0:def 3;

end;

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

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: verum

end;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: verum

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: verum

suppose
len D1 >= 2
; :: thesis: (Sum (upper_volume (f,D1))) - (Sum (upper_volume (f,D2))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1)

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: verum

end;