let x be Real; 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; 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; 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; ( 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
; (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 (Sum (upper_volume (f,D1))) - (Sum (upper_volume (f,D2))) <= ((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
;
(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
rng MD1 c= 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
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
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 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;
verum end; end; end;
hence
(Sum (upper_volume (f,D1))) - (Sum (upper_volume (f,D2))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1)
; verum