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 (lower_volume (f,D2))) - (Sum (lower_volume (f,D1))) <= ((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 (lower_volume (f,D2))) - (Sum (lower_volume (f,D1))) <= ((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 (lower_volume (f,D2))) - (Sum (lower_volume (f,D1))) <= ((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 (lower_volume (f,D2))) - (Sum (lower_volume (f,D1))) <= ((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 (lower_volume (f,D2))) - (Sum (lower_volume (f,D1))) <= ((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 (lower_volume (f,D2))) - (Sum (lower_volume (f,D1))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1)
per cases ( len D1 = 1 or len D1 >= 2 ) by A8;
suppose A9: len D1 = 1 ; :: thesis: (Sum (lower_volume (f,D2))) - (Sum (lower_volume (f,D1))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1)
then reconsider MD1 = <*()*> ^ D1 as non empty increasing FinSequence of REAL by ;
A10: len MD1 = () + (len D1) by FINSEQ_1:22;
(len <*()*>) + 1 <= () + (len D1) by ;
then MD1 . (len MD1) = D1 . ((() + (len D1)) - ()) by
.= 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 rng MD1 c= A ;
then reconsider MD1 = MD1 as Division of A by ;
A15: len MD1 = () + (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 ;
then (D1 . 1) - () > 0 by ;
then A17: lower_bound A < D1 . 1 by XREAL_1:47;
lower_volume (f,D1) = (lower_volume (f,MD1)) /^ 1 by Lm10;
then lower_volume (f,MD1) = <*((lower_volume (f,MD1)) /. 1)*> ^ (lower_volume (f,D1)) by FINSEQ_5:29;
then A18: Sum (lower_volume (f,MD1)) = ((lower_volume (f,MD1)) /. 1) + (Sum (lower_volume (f,D1))) by RVSUM_1:76;
A19: len D1 in dom D1 by FINSEQ_5:6;
A20: 1 + (len D1) >= 1 + 1 by ;
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
.= lower_bound A by ;
then A23: lower_bound (divset (D1,(len D1))) = lower_bound (divset (MD1,(len MD1))) by ;
set MD2 = <*()*> ^ D2;
rng MD1 <> {} ;
then A24: 1 in dom MD1 by FINSEQ_3:32;
then A25: (lower_volume (f,MD1)) . 1 = (lower_bound (rng (f | (divset (MD1,1))))) * (vol (divset (MD1,1))) by INTEGRA1:def 7;
1 in Seg (len MD1) by ;
then 1 in Seg (len (lower_volume (f,MD1))) by INTEGRA1:def 7;
then A26: 1 in dom (lower_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 <*()*>) + 1 <= () + (len D2) by XREAL_1:6;
A29: D2 . 1 in rng D2 by ;
lower_bound A < D2 . 1
proof
per cases ( D2 . 1 in rng D1 or D2 . 1 in {x} ) by ;
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 ;
1 <= k by ;
then D1 . 1 <= D2 . 1 by ;
hence lower_bound A < D2 . 1 by ; :: thesis: verum
end;
suppose D2 . 1 in {x} ; :: thesis: lower_bound A < D2 . 1
hence lower_bound A < D2 . 1 by ; :: thesis: verum
end;
end;
end;
then reconsider MD2 = <*()*> ^ D2 as non empty increasing FinSequence of REAL by Lm9;
len MD2 = () + (len D2) by FINSEQ_1:22;
then MD2 . (len MD2) = D2 . ((() + (len D2)) - ()) by
.= 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 rng MD2 c= A ;
then reconsider MD2 = MD2 as Division of A by ;
A38: x <= upper_bound (divset (D1,(len D1))) by ;
rng MD2 = (rng D2) \/ () by FINSEQ_1:31
.= ((rng D1) \/ ()) \/ {x} by ;
then A39: rng MD2 = (rng MD1) \/ {x} by FINSEQ_1:31;
MD1 . (len MD1) = MD1 . (() + (len D1)) by FINSEQ_1:22
.= D1 . (len D1) by ;
then A40: upper_bound (divset (MD1,(len MD1))) = D1 . (len D1) by
.= upper_bound (divset (D1,(len D1))) by ;
rng D1 c= rng D2 by ;
then (rng D1) \/ () c= (rng D2) \/ () by XBOOLE_1:9;
then rng MD1 c= (rng D2) \/ () by FINSEQ_1:31;
then A41: rng MD1 c= rng MD2 by FINSEQ_1:31;
len D1 <= len D2 by ;
then (len D1) + () <= (len D2) + () by XREAL_1:6;
then len MD1 <= (len D2) + () by FINSEQ_1:22;
then len MD1 <= len MD2 by FINSEQ_1:22;
then A42: MD1 <= MD2 by ;
lower_bound (divset (D1,(len D1))) <= x by ;
then x in divset (MD1,(len MD1)) by ;
then A43: (Sum (lower_volume (f,MD2))) - (Sum (lower_volume (f,MD1))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta MD1) by A5, A15, A20, A42, A39, Th10;
rng MD2 <> {} ;
then A44: 1 in dom MD2 by FINSEQ_3:32;
then A45: (lower_volume (f,MD2)) . 1 = (lower_bound (rng (f | (divset (MD2,1))))) * (vol (divset (MD2,1))) by INTEGRA1:def 7;
1 in Seg (len MD2) by ;
then 1 in Seg (len (lower_volume (f,MD2))) by INTEGRA1:def 7;
then A46: 1 in dom (lower_volume (f,MD2)) by FINSEQ_1:def 3;
vol (divset (MD2,1)) = 0 by Lm11;
then A47: (lower_volume (f,MD2)) /. 1 = 0 by ;
lower_volume (f,D2) = (lower_volume (f,MD2)) /^ 1 by Lm10;
then lower_volume (f,MD2) = <*((lower_volume (f,MD2)) /. 1)*> ^ (lower_volume (f,D2)) by FINSEQ_5:29;
then A48: Sum (lower_volume (f,MD2)) = ((lower_volume (f,MD2)) /. 1) + (Sum (lower_volume (f,D2))) by RVSUM_1:76;
vol (divset (MD1,1)) = 0 by Lm11;
then (lower_volume (f,MD1)) /. 1 = 0 by ;
hence (Sum (lower_volume (f,D2))) - (Sum (lower_volume (f,D1))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1) by A43, A18, A48, A47, Lm12; :: thesis: verum
end;
suppose len D1 >= 2 ; :: thesis: (Sum (lower_volume (f,D2))) - (Sum (lower_volume (f,D1))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1)
hence (Sum (lower_volume (f,D2))) - (Sum (lower_volume (f,D1))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1) by A1, A3, A4, A5, Th10; :: thesis: verum
end;
end;
end;
hence (Sum (lower_volume (f,D2))) - (Sum (lower_volume (f,D1))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1) ; :: thesis: verum