let A be non empty closed_interval Subset of REAL; :: thesis: for f being Function of A,REAL

for T being DivSequence of A st f | A is bounded & delta T is 0 -convergent & delta T is non-zero & vol A <> 0 holds

( upper_sum (f,T) is convergent & lim (upper_sum (f,T)) = upper_integral f )

let f be Function of A,REAL; :: thesis: for T being DivSequence of A st f | A is bounded & delta T is 0 -convergent & delta T is non-zero & vol A <> 0 holds

( upper_sum (f,T) is convergent & lim (upper_sum (f,T)) = upper_integral f )

let T be DivSequence of A; :: thesis: ( f | A is bounded & delta T is 0 -convergent & delta T is non-zero & vol A <> 0 implies ( upper_sum (f,T) is convergent & lim (upper_sum (f,T)) = upper_integral f ) )

assume A1: f | A is bounded ; :: thesis: ( not delta T is 0 -convergent or not delta T is non-zero or not vol A <> 0 or ( upper_sum (f,T) is convergent & lim (upper_sum (f,T)) = upper_integral f ) )

then A2: for D, D1 being Division of A ex D2 being Division of A st

( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & 0 <= (upper_sum (f,D)) - (upper_sum (f,D2)) & 0 <= (upper_sum (f,D1)) - (upper_sum (f,D2)) ) by Th22;

A7: for D, D1 being Division of A st delta D1 < min (rng (upper_volume ((chi (A,A)),D))) holds

ex D2 being Division of A st

( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & (upper_sum (f,D1)) - (upper_sum (f,D2)) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) ) by A1, Th23;

assume A559: ( delta T is 0 -convergent & delta T is non-zero ) ; :: thesis: ( not vol A <> 0 or ( upper_sum (f,T) is convergent & lim (upper_sum (f,T)) = upper_integral f ) )

then A560: delta T is convergent by FDIFF_1:def 1;

A561: lim (delta T) = 0 by A559, FDIFF_1:def 1;

assume A562: vol A <> 0 ; :: thesis: ( upper_sum (f,T) is convergent & lim (upper_sum (f,T)) = upper_integral f )

A563: delta T is non-zero by A559;

A564: for e being Real st e > 0 holds

ex n being Nat st

for m being Nat st n <= m holds

( 0 < (delta T) . m & (delta T) . m < e )

ex n being Nat st

for m being Nat st n <= m holds

|.(((upper_sum (f,T)) . m) - (upper_integral f)).| < e

hence lim (upper_sum (f,T)) = upper_integral f by A571, SEQ_2:def 7; :: thesis: verum

for T being DivSequence of A st f | A is bounded & delta T is 0 -convergent & delta T is non-zero & vol A <> 0 holds

( upper_sum (f,T) is convergent & lim (upper_sum (f,T)) = upper_integral f )

let f be Function of A,REAL; :: thesis: for T being DivSequence of A st f | A is bounded & delta T is 0 -convergent & delta T is non-zero & vol A <> 0 holds

( upper_sum (f,T) is convergent & lim (upper_sum (f,T)) = upper_integral f )

let T be DivSequence of A; :: thesis: ( f | A is bounded & delta T is 0 -convergent & delta T is non-zero & vol A <> 0 implies ( upper_sum (f,T) is convergent & lim (upper_sum (f,T)) = upper_integral f ) )

assume A1: f | A is bounded ; :: thesis: ( not delta T is 0 -convergent or not delta T is non-zero or not vol A <> 0 or ( upper_sum (f,T) is convergent & lim (upper_sum (f,T)) = upper_integral f ) )

then A2: for D, D1 being Division of A ex D2 being Division of A st

( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & 0 <= (upper_sum (f,D)) - (upper_sum (f,D2)) & 0 <= (upper_sum (f,D1)) - (upper_sum (f,D2)) ) by Th22;

A7: for D, D1 being Division of A st delta D1 < min (rng (upper_volume ((chi (A,A)),D))) holds

ex D2 being Division of A st

( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & (upper_sum (f,D1)) - (upper_sum (f,D2)) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) ) by A1, Th23;

assume A559: ( delta T is 0 -convergent & delta T is non-zero ) ; :: thesis: ( not vol A <> 0 or ( upper_sum (f,T) is convergent & lim (upper_sum (f,T)) = upper_integral f ) )

then A560: delta T is convergent by FDIFF_1:def 1;

A561: lim (delta T) = 0 by A559, FDIFF_1:def 1;

assume A562: vol A <> 0 ; :: thesis: ( upper_sum (f,T) is convergent & lim (upper_sum (f,T)) = upper_integral f )

A563: delta T is non-zero by A559;

A564: for e being Real st e > 0 holds

ex n being Nat st

for m being Nat st n <= m holds

( 0 < (delta T) . m & (delta T) . m < e )

proof

A571:
for e being Real st e > 0 holds
let e be Real; :: thesis: ( e > 0 implies ex n being Nat st

for m being Nat st n <= m holds

( 0 < (delta T) . m & (delta T) . m < e ) )

assume e > 0 ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

( 0 < (delta T) . m & (delta T) . m < e )

then consider n being Nat such that

A565: for m being Nat st n <= m holds

|.(((delta T) . m) - 0).| < e by A560, A561, SEQ_2:def 7;

take n ; :: thesis: for m being Nat st n <= m holds

( 0 < (delta T) . m & (delta T) . m < e )

let m be Nat; :: thesis: ( n <= m implies ( 0 < (delta T) . m & (delta T) . m < e ) )

reconsider mm = m as Element of NAT by ORDINAL1:def 12;

assume n <= m ; :: thesis: ( 0 < (delta T) . m & (delta T) . m < e )

then |.(((delta T) . m) - 0).| < e by A565;

then A566: ((delta T) . m) + |.(((delta T) . m) - 0).| < e + |.(((delta T) . m) - 0).| by ABSVALUE:4, XREAL_1:8;

reconsider D = T . mm as Division of A ;

A567: (delta T) . m = delta (T . mm) by Def2;

delta (T . mm) in rng (upper_volume ((chi (A,A)),(T . mm))) by XXREAL_2:def 8;

then consider i being Element of NAT such that

A568: i in dom (upper_volume ((chi (A,A)),(T . mm))) and

A569: delta (T . mm) = (upper_volume ((chi (A,A)),(T . mm))) . i by PARTFUN1:3;

i in Seg (len (upper_volume ((chi (A,A)),(T . mm)))) by A568, FINSEQ_1:def 3;

then i in Seg (len D) by INTEGRA1:def 6;

then i in dom D by FINSEQ_1:def 3;

then A570: delta (T . mm) = vol (divset ((T . mm),i)) by A569, INTEGRA1:20;

(delta T) . m <> 0 by A563, SEQ_1:5;

hence ( 0 < (delta T) . m & (delta T) . m < e ) by A566, A567, A570, INTEGRA1:9, XREAL_1:6; :: thesis: verum

end;for m being Nat st n <= m holds

( 0 < (delta T) . m & (delta T) . m < e ) )

assume e > 0 ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

( 0 < (delta T) . m & (delta T) . m < e )

then consider n being Nat such that

A565: for m being Nat st n <= m holds

|.(((delta T) . m) - 0).| < e by A560, A561, SEQ_2:def 7;

take n ; :: thesis: for m being Nat st n <= m holds

( 0 < (delta T) . m & (delta T) . m < e )

let m be Nat; :: thesis: ( n <= m implies ( 0 < (delta T) . m & (delta T) . m < e ) )

reconsider mm = m as Element of NAT by ORDINAL1:def 12;

assume n <= m ; :: thesis: ( 0 < (delta T) . m & (delta T) . m < e )

then |.(((delta T) . m) - 0).| < e by A565;

then A566: ((delta T) . m) + |.(((delta T) . m) - 0).| < e + |.(((delta T) . m) - 0).| by ABSVALUE:4, XREAL_1:8;

reconsider D = T . mm as Division of A ;

A567: (delta T) . m = delta (T . mm) by Def2;

delta (T . mm) in rng (upper_volume ((chi (A,A)),(T . mm))) by XXREAL_2:def 8;

then consider i being Element of NAT such that

A568: i in dom (upper_volume ((chi (A,A)),(T . mm))) and

A569: delta (T . mm) = (upper_volume ((chi (A,A)),(T . mm))) . i by PARTFUN1:3;

i in Seg (len (upper_volume ((chi (A,A)),(T . mm)))) by A568, FINSEQ_1:def 3;

then i in Seg (len D) by INTEGRA1:def 6;

then i in dom D by FINSEQ_1:def 3;

then A570: delta (T . mm) = vol (divset ((T . mm),i)) by A569, INTEGRA1:20;

(delta T) . m <> 0 by A563, SEQ_1:5;

hence ( 0 < (delta T) . m & (delta T) . m < e ) by A566, A567, A570, INTEGRA1:9, XREAL_1:6; :: thesis: verum

ex n being Nat st

for m being Nat st n <= m holds

|.(((upper_sum (f,T)) . m) - (upper_integral f)).| < e

proof

hence
upper_sum (f,T) is convergent
by SEQ_2:def 6; :: thesis: lim (upper_sum (f,T)) = upper_integral f
let e be Real; :: thesis: ( e > 0 implies ex n being Nat st

for m being Nat st n <= m holds

|.(((upper_sum (f,T)) . m) - (upper_integral f)).| < e )

assume A572: e > 0 ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

|.(((upper_sum (f,T)) . m) - (upper_integral f)).| < e

then A573: e / 2 > 0 by XREAL_1:139;

reconsider e = e as Real ;

A574: rng (upper_sum_set f) is bounded_below by A1, INTEGRA2:35;

upper_integral f = lower_bound (rng (upper_sum_set f)) by INTEGRA1:def 14;

then consider y being Real such that

A575: y in rng (upper_sum_set f) and

A576: (upper_integral f) + (e / 2) > y by A573, A574, SEQ_4:def 2;

ex D being Division of A st

( D in dom (upper_sum_set f) & y = (upper_sum_set f) . D & D . 1 > lower_bound A )

D in dom (upper_sum_set f) and

A627: y = (upper_sum_set f) . D and

A628: D . 1 > lower_bound A ;

deffunc H_{1}( Nat) -> Element of REAL = In ((vol (divset (D,$1))),REAL);

set p = len D;

set H = upper_bound (rng f);

set h = lower_bound (rng f);

consider v being FinSequence of REAL such that

A629: ( len v = len D & ( for j being Nat st j in dom v holds

v . j = H_{1}(j) ) )
from FINSEQ_2:sch 1();

A630: 2 * (len D) > 0 by XREAL_1:129;

consider v1 being non-decreasing FinSequence of REAL such that

A631: v,v1 are_fiberwise_equipotent by INTEGRA2:3;

defpred S_{1}[ Nat] means ( $1 in dom v1 & v1 . $1 > 0 );

A632: dom v = Seg (len D) by A629, FINSEQ_1:def 3;

A633: ex k being Nat st S_{1}[k]

A638: ( S_{1}[k] & ( for n being Nat st S_{1}[n] holds

k <= n ) ) from NAT_1:sch 5(A633);

A639: (upper_bound (rng f)) - (lower_bound (rng f)) >= 0 by A1, Lm3, XREAL_1:48;

then A640: (2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1) > 0 by A630, XREAL_1:129;

min ((v1 . k),(e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)))) > 0

A641: for m being Nat st n <= m holds

( 0 < (delta T) . m & (delta T) . m < min ((v1 . k),(e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)))) ) by A564;

take n ; :: thesis: for m being Nat st n <= m holds

|.(((upper_sum (f,T)) . m) - (upper_integral f)).| < e

A642: y = upper_sum (f,D) by A627, INTEGRA1:def 10;

A643: v1 . 1 > 0

set s = upper_integral f;

set sD = upper_sum (f,D);

let m be Nat; :: thesis: ( n <= m implies |.(((upper_sum (f,T)) . m) - (upper_integral f)).| < e )

reconsider mm = m as Element of NAT by ORDINAL1:def 12;

reconsider D1 = T . mm as Division of A ;

A677: delta D1 = (delta T) . m by Def2;

consider D2 being Division of A such that

A678: D <= D2 and

D1 <= D2 and

A679: rng D2 = (rng D1) \/ (rng D) and

0 <= (upper_sum (f,D)) - (upper_sum (f,D2)) and

0 <= (upper_sum (f,D1)) - (upper_sum (f,D2)) by A2;

set sD1 = upper_sum (f,(T . mm));

set sD2 = upper_sum (f,D2);

upper_sum (f,D2) <= upper_sum (f,D) by A1, A678, INTEGRA1:45;

then A680: (upper_sum (f,(T . mm))) - (upper_sum (f,D)) <= (upper_sum (f,(T . mm))) - (upper_sum (f,D2)) by XREAL_1:10;

(((upper_sum (f,D)) + (upper_sum (f,(T . mm)))) - (upper_sum (f,(T . mm)))) - (upper_integral f) < e / 2 by A576, A642, XREAL_1:19;

then (((upper_sum (f,(T . mm))) - (upper_integral f)) + (upper_sum (f,D))) - (upper_sum (f,(T . mm))) < e / 2 ;

then ((upper_sum (f,(T . mm))) - (upper_integral f)) + (upper_sum (f,D)) < (upper_sum (f,(T . mm))) + (e / 2) by XREAL_1:19;

then A681: (upper_sum (f,(T . mm))) - (upper_integral f) < ((upper_sum (f,(T . mm))) + (e / 2)) - (upper_sum (f,D)) by XREAL_1:20;

T . mm in divs A by INTEGRA1:def 3;

then A682: T . m in dom (upper_sum_set f) by FUNCT_2:def 1;

(upper_sum (f,T)) . m = upper_sum (f,(T . mm)) by INTEGRA2:def 2;

then (upper_sum (f,T)) . m = (upper_sum_set f) . (T . m) by INTEGRA1:def 10;

then (upper_sum (f,T)) . m in rng (upper_sum_set f) by A682, FUNCT_1:def 3;

then lower_bound (rng (upper_sum_set f)) <= (upper_sum (f,T)) . m by A574, SEQ_4:def 2;

then upper_integral f <= (upper_sum (f,T)) . m by INTEGRA1:def 14;

then A683: ((upper_sum (f,T)) . m) - (upper_integral f) >= 0 by XREAL_1:48;

(upper_bound (rng f)) - (lower_bound (rng f)) <= ((upper_bound (rng f)) - (lower_bound (rng f))) + 1 by XREAL_1:29;

then A684: (len D) * ((upper_bound (rng f)) - (lower_bound (rng f))) <= (len D) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1) by XREAL_1:64;

A685: min ((v1 . k),(e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)))) <= e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)) by XXREAL_0:17;

assume A686: n <= m ; :: thesis: |.(((upper_sum (f,T)) . m) - (upper_integral f)).| < e

then (delta T) . m < min ((v1 . k),(e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)))) by A641;

then (delta T) . m < e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)) by A685, XXREAL_0:2;

then ((delta T) . m) * ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)) < e by A630, A639, XREAL_1:79, XREAL_1:129;

then (((delta T) . m) * ((len D) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1))) * 2 < e ;

then A687: ((len D) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)) * ((delta T) . m) < e / 2 by XREAL_1:81;

(delta T) . m < min ((v1 . k),(e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)))) by A641, A686;

then delta D1 < v1 . k by A677, A676, XXREAL_0:2;

then ex D3 being Division of A st

( D <= D3 & D1 <= D3 & rng D3 = (rng D1) \/ (rng D) & (upper_sum (f,D1)) - (upper_sum (f,D3)) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) ) by A7, A658;

then A688: (upper_sum (f,D1)) - (upper_sum (f,D2)) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) by A679, Th6;

0 < (delta T) . m by A641, A686;

then ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * ((delta T) . m) <= ((len D) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)) * ((delta T) . m) by A684, XREAL_1:64;

then (upper_sum (f,(T . mm))) - (upper_sum (f,D2)) <= ((len D) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)) * ((delta T) . m) by A677, A688, XXREAL_0:2;

then (upper_sum (f,(T . mm))) - (upper_sum (f,D)) <= ((len D) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)) * ((delta T) . m) by A680, XXREAL_0:2;

then (upper_sum (f,(T . mm))) - (upper_sum (f,D)) < e / 2 by A687, XXREAL_0:2;

then ((upper_sum (f,(T . mm))) - (upper_sum (f,D))) + (e / 2) < (e / 2) + (e / 2) by XREAL_1:6;

then (upper_sum (f,(T . mm))) - (upper_integral f) < e by A681, XXREAL_0:2;

then ((upper_sum (f,T)) . m) - (upper_integral f) < e by INTEGRA2:def 2;

hence |.(((upper_sum (f,T)) . m) - (upper_integral f)).| < e by A683, ABSVALUE:def 1; :: thesis: verum

end;for m being Nat st n <= m holds

|.(((upper_sum (f,T)) . m) - (upper_integral f)).| < e )

assume A572: e > 0 ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

|.(((upper_sum (f,T)) . m) - (upper_integral f)).| < e

then A573: e / 2 > 0 by XREAL_1:139;

reconsider e = e as Real ;

A574: rng (upper_sum_set f) is bounded_below by A1, INTEGRA2:35;

upper_integral f = lower_bound (rng (upper_sum_set f)) by INTEGRA1:def 14;

then consider y being Real such that

A575: y in rng (upper_sum_set f) and

A576: (upper_integral f) + (e / 2) > y by A573, A574, SEQ_4:def 2;

ex D being Division of A st

( D in dom (upper_sum_set f) & y = (upper_sum_set f) . D & D . 1 > lower_bound A )

proof

then consider D being Division of A such that
consider D3 being Element of divs A such that

A577: D3 in dom (upper_sum_set f) and

A578: y = (upper_sum_set f) . D3 by A575, PARTFUN1:3;

reconsider D3 = D3 as Division of A by INTEGRA1:def 3;

A579: len D3 in Seg (len D3) by FINSEQ_1:3;

then 1 <= len D3 by FINSEQ_1:1;

then 1 in Seg (len D3) by FINSEQ_1:1;

then A580: 1 in dom D3 by FINSEQ_1:def 3;

end;A577: D3 in dom (upper_sum_set f) and

A578: y = (upper_sum_set f) . D3 by A575, PARTFUN1:3;

reconsider D3 = D3 as Division of A by INTEGRA1:def 3;

A579: len D3 in Seg (len D3) by FINSEQ_1:3;

then 1 <= len D3 by FINSEQ_1:1;

then 1 in Seg (len D3) by FINSEQ_1:1;

then A580: 1 in dom D3 by FINSEQ_1:def 3;

per cases
( D3 . 1 <> lower_bound A or D3 . 1 = lower_bound A )
;

end;

suppose A581:
D3 . 1 <> lower_bound A
; :: thesis: ex D being Division of A st

( D in dom (upper_sum_set f) & y = (upper_sum_set f) . D & D . 1 > lower_bound A )

( D in dom (upper_sum_set f) & y = (upper_sum_set f) . D & D . 1 > lower_bound A )

D3 . 1 in A
by A580, INTEGRA1:6;

then lower_bound A <= D3 . 1 by INTEGRA2:1;

then D3 . 1 > lower_bound A by A581, XXREAL_0:1;

hence ex D being Division of A st

( D in dom (upper_sum_set f) & y = (upper_sum_set f) . D & D . 1 > lower_bound A ) by A577, A578; :: thesis: verum

end;then lower_bound A <= D3 . 1 by INTEGRA2:1;

then D3 . 1 > lower_bound A by A581, XXREAL_0:1;

hence ex D being Division of A st

( D in dom (upper_sum_set f) & y = (upper_sum_set f) . D & D . 1 > lower_bound A ) by A577, A578; :: thesis: verum

suppose A582:
D3 . 1 = lower_bound A
; :: thesis: ex D being Division of A st

( D in dom (upper_sum_set f) & y = (upper_sum_set f) . D & D . 1 > lower_bound A )

( D in dom (upper_sum_set f) & y = (upper_sum_set f) . D & D . 1 > lower_bound A )

ex D being Division of A st

( D in dom (upper_sum_set f) & y = (upper_sum_set f) . D & D . 1 > lower_bound A )

( D in dom (upper_sum_set f) & y = (upper_sum_set f) . D & D . 1 > lower_bound A ) ; :: thesis: verum

end;( D in dom (upper_sum_set f) & y = (upper_sum_set f) . D & D . 1 > lower_bound A )

proof

hence
ex D being Division of A st
A583:
(upper_volume (f,D3)) . 1 = (upper_bound (rng (f | (divset (D3,1))))) * (vol (divset (D3,1)))
by A580, INTEGRA1:def 6;

vol A >= 0 by INTEGRA1:9;

then A584: (upper_bound A) - (lower_bound A) > 0 by A562, INTEGRA1:def 5;

A585: y = upper_sum (f,D3) by A578, INTEGRA1:def 10

.= Sum (upper_volume (f,D3)) by INTEGRA1:def 8

.= Sum (((upper_volume (f,D3)) | 1) ^ ((upper_volume (f,D3)) /^ 1)) by RFINSEQ:8 ;

A586: D3 . (len D3) = upper_bound A by INTEGRA1:def 2;

len D3 in dom D3 by A579, FINSEQ_1:def 3;

then A587: len D3 > 1 by A580, A582, A586, A584, SEQ_4:137, XREAL_1:47;

then reconsider D = D3 /^ 1 as increasing FinSequence of REAL by INTEGRA1:34;

A588: len D = (len D3) - 1 by A587, RFINSEQ:def 1;

upper_bound A > lower_bound A by A584, XREAL_1:47;

then len D <> 0 by A582, A588, INTEGRA1:def 2;

then reconsider D = D as non empty increasing FinSequence of REAL ;

A589: len D in dom D by FINSEQ_5:6;

(len D) + 1 = len D3 by A588;

then A590: D . (len D) = upper_bound A by A586, A587, A589, RFINSEQ:def 1;

A591: len D in Seg (len D) by FINSEQ_1:3;

1 + 1 <= len D3 by A587, NAT_1:13;

then 2 in dom D3 by FINSEQ_3:25;

then A592: D3 . 1 < D3 . 2 by A580, SEQM_3:def 1;

A593: rng D3 c= A by INTEGRA1:def 2;

rng D c= rng D3 by FINSEQ_5:33;

then rng D c= A by A593;

then reconsider D = D as Division of A by A590, INTEGRA1:def 2;

A594: 1 in Seg 1 by FINSEQ_1:1;

A595: len D3 >= 1 + 1 by A587, NAT_1:13;

then A596: 2 <= len (upper_volume (f,D3)) by INTEGRA1:def 6;

1 <= len (upper_volume (f,D3)) by A587, INTEGRA1:def 6;

then A597: len (mid ((upper_volume (f,D3)),2,(len (upper_volume (f,D3))))) = ((len (upper_volume (f,D3))) -' 2) + 1 by A596, FINSEQ_6:118

.= ((len D3) -' 2) + 1 by INTEGRA1:def 6

.= ((len D3) - 2) + 1 by A595, XREAL_1:233

.= (len D3) - 1 ;

A598: for i being Nat st 1 <= i & i <= len (mid ((upper_volume (f,D3)),2,(len (upper_volume (f,D3))))) holds

(mid ((upper_volume (f,D3)),2,(len (upper_volume (f,D3))))) . i = (upper_volume (f,D)) . i

A620: len ((upper_volume (f,D3)) | 1) = 1 ;

1 in dom (upper_volume (f,D3)) by A619, FINSEQ_3:25;

then ((upper_volume (f,D3)) | 1) . 1 = (upper_volume (f,D3)) . 1 by A594, RFINSEQ:6;

then A621: (upper_volume (f,D3)) | 1 = <*((upper_volume (f,D3)) . 1)*> by A620, FINSEQ_1:40;

A622: 2 -' 1 = 2 - 1 by XREAL_1:233

.= 1 ;

1 <= len D by A591, FINSEQ_1:1;

then 1 in dom D by FINSEQ_3:25;

then A623: D . 1 = D3 . (1 + 1) by A587, RFINSEQ:def 1

.= D3 . 2 ;

D in divs A by INTEGRA1:def 3;

then A624: D in dom (upper_sum_set f) by FUNCT_2:def 1;

len (upper_volume (f,D3)) >= 2 by A595, INTEGRA1:def 6;

then A625: mid ((upper_volume (f,D3)),2,(len (upper_volume (f,D3)))) = (upper_volume (f,D3)) /^ 1 by A622, FINSEQ_6:117;

len (mid ((upper_volume (f,D3)),2,(len (upper_volume (f,D3))))) = len (upper_volume (f,D)) by A588, A597, INTEGRA1:def 6;

then A626: (upper_volume (f,D3)) /^ 1 = upper_volume (f,D) by A625, A598, FINSEQ_1:14;

vol (divset (D3,1)) = (upper_bound (divset (D3,1))) - (lower_bound (divset (D3,1))) by INTEGRA1:def 5

.= (upper_bound (divset (D3,1))) - (lower_bound A) by A580, INTEGRA1:def 4

.= (D3 . 1) - (lower_bound A) by A580, INTEGRA1:def 4

.= 0 by A582 ;

then y = 0 + (Sum (upper_volume (f,D))) by A585, A621, A583, A626, RVSUM_1:76

.= upper_sum (f,D) by INTEGRA1:def 8 ;

then y = (upper_sum_set f) . D by INTEGRA1:def 10;

hence ex D being Division of A st

( D in dom (upper_sum_set f) & y = (upper_sum_set f) . D & D . 1 > lower_bound A ) by A582, A624, A623, A592; :: thesis: verum

end;vol A >= 0 by INTEGRA1:9;

then A584: (upper_bound A) - (lower_bound A) > 0 by A562, INTEGRA1:def 5;

A585: y = upper_sum (f,D3) by A578, INTEGRA1:def 10

.= Sum (upper_volume (f,D3)) by INTEGRA1:def 8

.= Sum (((upper_volume (f,D3)) | 1) ^ ((upper_volume (f,D3)) /^ 1)) by RFINSEQ:8 ;

A586: D3 . (len D3) = upper_bound A by INTEGRA1:def 2;

len D3 in dom D3 by A579, FINSEQ_1:def 3;

then A587: len D3 > 1 by A580, A582, A586, A584, SEQ_4:137, XREAL_1:47;

then reconsider D = D3 /^ 1 as increasing FinSequence of REAL by INTEGRA1:34;

A588: len D = (len D3) - 1 by A587, RFINSEQ:def 1;

upper_bound A > lower_bound A by A584, XREAL_1:47;

then len D <> 0 by A582, A588, INTEGRA1:def 2;

then reconsider D = D as non empty increasing FinSequence of REAL ;

A589: len D in dom D by FINSEQ_5:6;

(len D) + 1 = len D3 by A588;

then A590: D . (len D) = upper_bound A by A586, A587, A589, RFINSEQ:def 1;

A591: len D in Seg (len D) by FINSEQ_1:3;

1 + 1 <= len D3 by A587, NAT_1:13;

then 2 in dom D3 by FINSEQ_3:25;

then A592: D3 . 1 < D3 . 2 by A580, SEQM_3:def 1;

A593: rng D3 c= A by INTEGRA1:def 2;

rng D c= rng D3 by FINSEQ_5:33;

then rng D c= A by A593;

then reconsider D = D as Division of A by A590, INTEGRA1:def 2;

A594: 1 in Seg 1 by FINSEQ_1:1;

A595: len D3 >= 1 + 1 by A587, NAT_1:13;

then A596: 2 <= len (upper_volume (f,D3)) by INTEGRA1:def 6;

1 <= len (upper_volume (f,D3)) by A587, INTEGRA1:def 6;

then A597: len (mid ((upper_volume (f,D3)),2,(len (upper_volume (f,D3))))) = ((len (upper_volume (f,D3))) -' 2) + 1 by A596, FINSEQ_6:118

.= ((len D3) -' 2) + 1 by INTEGRA1:def 6

.= ((len D3) - 2) + 1 by A595, XREAL_1:233

.= (len D3) - 1 ;

A598: for i being Nat st 1 <= i & i <= len (mid ((upper_volume (f,D3)),2,(len (upper_volume (f,D3))))) holds

(mid ((upper_volume (f,D3)),2,(len (upper_volume (f,D3))))) . i = (upper_volume (f,D)) . i

proof

A619:
1 <= len (upper_volume (f,D3))
by A587, INTEGRA1:def 6;
let i be Nat; :: thesis: ( 1 <= i & i <= len (mid ((upper_volume (f,D3)),2,(len (upper_volume (f,D3))))) implies (mid ((upper_volume (f,D3)),2,(len (upper_volume (f,D3))))) . i = (upper_volume (f,D)) . i )

assume that

A599: 1 <= i and

A600: i <= len (mid ((upper_volume (f,D3)),2,(len (upper_volume (f,D3))))) ; :: thesis: (mid ((upper_volume (f,D3)),2,(len (upper_volume (f,D3))))) . i = (upper_volume (f,D)) . i

A601: 1 <= i + 1 by NAT_1:12;

i + 1 <= len D3 by A597, A600, XREAL_1:19;

then A602: i + 1 in Seg (len D3) by A601, FINSEQ_1:1;

then A603: i + 1 in dom D3 by FINSEQ_1:def 3;

A604: divset (D3,(i + 1)) = divset (D,i)

then A617: i <= ((len (upper_volume (f,D3))) - 2) + 1 ;

(mid ((upper_volume (f,D3)),2,(len (upper_volume (f,D3))))) . i = (upper_volume (f,D3)) . ((i + 2) - 1) by A596, A599, A617, FINSEQ_6:122

.= (upper_volume (f,D3)) . (i + 1) ;

then A618: (mid ((upper_volume (f,D3)),2,(len (upper_volume (f,D3))))) . i = (upper_bound (rng (f | (divset (D3,(i + 1)))))) * (vol (divset (D3,(i + 1)))) by A603, INTEGRA1:def 6;

i in Seg (len D) by A588, A597, A599, A600, FINSEQ_1:1;

then i in dom D by FINSEQ_1:def 3;

hence (mid ((upper_volume (f,D3)),2,(len (upper_volume (f,D3))))) . i = (upper_volume (f,D)) . i by A618, A604, INTEGRA1:def 6; :: thesis: verum

end;assume that

A599: 1 <= i and

A600: i <= len (mid ((upper_volume (f,D3)),2,(len (upper_volume (f,D3))))) ; :: thesis: (mid ((upper_volume (f,D3)),2,(len (upper_volume (f,D3))))) . i = (upper_volume (f,D)) . i

A601: 1 <= i + 1 by NAT_1:12;

i + 1 <= len D3 by A597, A600, XREAL_1:19;

then A602: i + 1 in Seg (len D3) by A601, FINSEQ_1:1;

then A603: i + 1 in dom D3 by FINSEQ_1:def 3;

A604: divset (D3,(i + 1)) = divset (D,i)

proof

i <= (len (upper_volume (f,D3))) - 1
by A597, A600, INTEGRA1:def 6;
A605:
i + 1 in dom D3
by A602, FINSEQ_1:def 3;

A606: 1 <> i + 1 by A599, NAT_1:13;

then A607: upper_bound (divset (D3,(i + 1))) = D3 . (i + 1) by A605, INTEGRA1:def 4;

A608: i in dom D by A588, A597, A599, A600, FINSEQ_3:25;

then A609: D . i = D3 . (i + 1) by A587, RFINSEQ:def 1;

A610: lower_bound (divset (D3,(i + 1))) = D3 . ((i + 1) - 1) by A606, A605, INTEGRA1:def 4;

end;A606: 1 <> i + 1 by A599, NAT_1:13;

then A607: upper_bound (divset (D3,(i + 1))) = D3 . (i + 1) by A605, INTEGRA1:def 4;

A608: i in dom D by A588, A597, A599, A600, FINSEQ_3:25;

then A609: D . i = D3 . (i + 1) by A587, RFINSEQ:def 1;

A610: lower_bound (divset (D3,(i + 1))) = D3 . ((i + 1) - 1) by A606, A605, INTEGRA1:def 4;

per cases
( i = 1 or i <> 1 )
;

end;

suppose A611:
i = 1
; :: thesis: divset (D3,(i + 1)) = divset (D,i)

then A612:
upper_bound (divset (D,i)) = D . i
by A608, INTEGRA1:def 4;

A613: lower_bound (divset (D,i)) = lower_bound A by A608, A611, INTEGRA1:def 4;

divset (D3,(i + 1)) = [.(lower_bound A),(D . i).] by A582, A607, A610, A609, A611, INTEGRA1:4;

hence divset (D3,(i + 1)) = divset (D,i) by A613, A612, INTEGRA1:4; :: thesis: verum

end;A613: lower_bound (divset (D,i)) = lower_bound A by A608, A611, INTEGRA1:def 4;

divset (D3,(i + 1)) = [.(lower_bound A),(D . i).] by A582, A607, A610, A609, A611, INTEGRA1:4;

hence divset (D3,(i + 1)) = divset (D,i) by A613, A612, INTEGRA1:4; :: thesis: verum

suppose A614:
i <> 1
; :: thesis: divset (D3,(i + 1)) = divset (D,i)

then
i - 1 in dom D
by A608, INTEGRA1:7;

then A615: D . (i - 1) = D3 . ((i - 1) + 1) by A587, RFINSEQ:def 1

.= D3 . i ;

A616: upper_bound (divset (D,i)) = D . i by A608, A614, INTEGRA1:def 4;

lower_bound (divset (D,i)) = D . (i - 1) by A608, A614, INTEGRA1:def 4;

then divset (D3,(i + 1)) = [.(lower_bound (divset (D,i))),(upper_bound (divset (D,i))).] by A607, A610, A609, A616, A615, INTEGRA1:4;

hence divset (D3,(i + 1)) = divset (D,i) by INTEGRA1:4; :: thesis: verum

end;then A615: D . (i - 1) = D3 . ((i - 1) + 1) by A587, RFINSEQ:def 1

.= D3 . i ;

A616: upper_bound (divset (D,i)) = D . i by A608, A614, INTEGRA1:def 4;

lower_bound (divset (D,i)) = D . (i - 1) by A608, A614, INTEGRA1:def 4;

then divset (D3,(i + 1)) = [.(lower_bound (divset (D,i))),(upper_bound (divset (D,i))).] by A607, A610, A609, A616, A615, INTEGRA1:4;

hence divset (D3,(i + 1)) = divset (D,i) by INTEGRA1:4; :: thesis: verum

then A617: i <= ((len (upper_volume (f,D3))) - 2) + 1 ;

(mid ((upper_volume (f,D3)),2,(len (upper_volume (f,D3))))) . i = (upper_volume (f,D3)) . ((i + 2) - 1) by A596, A599, A617, FINSEQ_6:122

.= (upper_volume (f,D3)) . (i + 1) ;

then A618: (mid ((upper_volume (f,D3)),2,(len (upper_volume (f,D3))))) . i = (upper_bound (rng (f | (divset (D3,(i + 1)))))) * (vol (divset (D3,(i + 1)))) by A603, INTEGRA1:def 6;

i in Seg (len D) by A588, A597, A599, A600, FINSEQ_1:1;

then i in dom D by FINSEQ_1:def 3;

hence (mid ((upper_volume (f,D3)),2,(len (upper_volume (f,D3))))) . i = (upper_volume (f,D)) . i by A618, A604, INTEGRA1:def 6; :: thesis: verum

A620: len ((upper_volume (f,D3)) | 1) = 1 ;

1 in dom (upper_volume (f,D3)) by A619, FINSEQ_3:25;

then ((upper_volume (f,D3)) | 1) . 1 = (upper_volume (f,D3)) . 1 by A594, RFINSEQ:6;

then A621: (upper_volume (f,D3)) | 1 = <*((upper_volume (f,D3)) . 1)*> by A620, FINSEQ_1:40;

A622: 2 -' 1 = 2 - 1 by XREAL_1:233

.= 1 ;

1 <= len D by A591, FINSEQ_1:1;

then 1 in dom D by FINSEQ_3:25;

then A623: D . 1 = D3 . (1 + 1) by A587, RFINSEQ:def 1

.= D3 . 2 ;

D in divs A by INTEGRA1:def 3;

then A624: D in dom (upper_sum_set f) by FUNCT_2:def 1;

len (upper_volume (f,D3)) >= 2 by A595, INTEGRA1:def 6;

then A625: mid ((upper_volume (f,D3)),2,(len (upper_volume (f,D3)))) = (upper_volume (f,D3)) /^ 1 by A622, FINSEQ_6:117;

len (mid ((upper_volume (f,D3)),2,(len (upper_volume (f,D3))))) = len (upper_volume (f,D)) by A588, A597, INTEGRA1:def 6;

then A626: (upper_volume (f,D3)) /^ 1 = upper_volume (f,D) by A625, A598, FINSEQ_1:14;

vol (divset (D3,1)) = (upper_bound (divset (D3,1))) - (lower_bound (divset (D3,1))) by INTEGRA1:def 5

.= (upper_bound (divset (D3,1))) - (lower_bound A) by A580, INTEGRA1:def 4

.= (D3 . 1) - (lower_bound A) by A580, INTEGRA1:def 4

.= 0 by A582 ;

then y = 0 + (Sum (upper_volume (f,D))) by A585, A621, A583, A626, RVSUM_1:76

.= upper_sum (f,D) by INTEGRA1:def 8 ;

then y = (upper_sum_set f) . D by INTEGRA1:def 10;

hence ex D being Division of A st

( D in dom (upper_sum_set f) & y = (upper_sum_set f) . D & D . 1 > lower_bound A ) by A582, A624, A623, A592; :: thesis: verum

( D in dom (upper_sum_set f) & y = (upper_sum_set f) . D & D . 1 > lower_bound A ) ; :: thesis: verum

D in dom (upper_sum_set f) and

A627: y = (upper_sum_set f) . D and

A628: D . 1 > lower_bound A ;

deffunc H

set p = len D;

set H = upper_bound (rng f);

set h = lower_bound (rng f);

consider v being FinSequence of REAL such that

A629: ( len v = len D & ( for j being Nat st j in dom v holds

v . j = H

A630: 2 * (len D) > 0 by XREAL_1:129;

consider v1 being non-decreasing FinSequence of REAL such that

A631: v,v1 are_fiberwise_equipotent by INTEGRA2:3;

defpred S

A632: dom v = Seg (len D) by A629, FINSEQ_1:def 3;

A633: ex k being Nat st S

proof

consider k being Nat such that
consider H being Function such that

dom H = dom v and

rng H = dom v1 and

H is one-to-one and

A634: v = v1 * H by A631, CLASSES1:77;

consider k being Element of NAT such that

A635: k in dom D and

A636: vol (divset (D,k)) > 0 by A562, Th2;

A637: dom D = Seg (len D) by FINSEQ_1:def 3;

then H . k in dom v1 by A632, A634, A635, FUNCT_1:11;

then reconsider Hk = H . k as Element of NAT ;

v . k = H_{1}(k)
by A629, A632, A635, A637;

then v . k > 0 by A636;

then S_{1}[Hk]
by A632, A634, A635, A637, FUNCT_1:11, FUNCT_1:12;

hence ex k being Nat st S_{1}[k]
; :: thesis: verum

end;dom H = dom v and

rng H = dom v1 and

H is one-to-one and

A634: v = v1 * H by A631, CLASSES1:77;

consider k being Element of NAT such that

A635: k in dom D and

A636: vol (divset (D,k)) > 0 by A562, Th2;

A637: dom D = Seg (len D) by FINSEQ_1:def 3;

then H . k in dom v1 by A632, A634, A635, FUNCT_1:11;

then reconsider Hk = H . k as Element of NAT ;

v . k = H

then v . k > 0 by A636;

then S

hence ex k being Nat st S

A638: ( S

k <= n ) ) from NAT_1:sch 5(A633);

A639: (upper_bound (rng f)) - (lower_bound (rng f)) >= 0 by A1, Lm3, XREAL_1:48;

then A640: (2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1) > 0 by A630, XREAL_1:129;

min ((v1 . k),(e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)))) > 0

proof
end;

then consider n being Nat such that per cases
( min ((v1 . k),(e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)))) = v1 . k or min ((v1 . k),(e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)))) = e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)) )
by XXREAL_0:15;

end;

suppose
min ((v1 . k),(e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)))) = v1 . k
; :: thesis: min ((v1 . k),(e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)))) > 0

hence
min ((v1 . k),(e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)))) > 0
by A638; :: thesis: verum

end;suppose
min ((v1 . k),(e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)))) = e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1))
; :: thesis: min ((v1 . k),(e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)))) > 0

hence
min ((v1 . k),(e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)))) > 0
by A572, A640, XREAL_1:139; :: thesis: verum

end;A641: for m being Nat st n <= m holds

( 0 < (delta T) . m & (delta T) . m < min ((v1 . k),(e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)))) ) by A564;

take n ; :: thesis: for m being Nat st n <= m holds

|.(((upper_sum (f,T)) . m) - (upper_integral f)).| < e

A642: y = upper_sum (f,D) by A627, INTEGRA1:def 10;

A643: v1 . 1 > 0

proof

A658:
v1 . k = min (rng (upper_volume ((chi (A,A)),D)))
A644:
for n1 being Element of NAT st n1 in dom D holds

vol (divset (D,n1)) > 0

1 <= k by A638, FINSEQ_3:25;

then 1 <= len v1 by A653, XXREAL_0:2;

then 1 in dom v1 by FINSEQ_3:25;

then A654: v1 . 1 in rng v1 by FUNCT_1:def 3;

rng v = rng v1 by A631, CLASSES1:75;

then consider n1 being Element of NAT such that

A655: n1 in dom v and

A656: v1 . 1 = v . n1 by A654, PARTFUN1:3;

n1 in Seg (len D) by A629, A655, FINSEQ_1:def 3;

then A657: n1 in dom D by FINSEQ_1:def 3;

v1 . 1 = H_{1}(n1)
by A629, A655, A656

.= vol (divset (D,n1)) ;

hence v1 . 1 > 0 by A644, A657; :: thesis: verum

end;vol (divset (D,n1)) > 0

proof

A653:
k <= len v1
by A638, FINSEQ_3:25;
let n1 be Element of NAT ; :: thesis: ( n1 in dom D implies vol (divset (D,n1)) > 0 )

assume A645: n1 in dom D ; :: thesis: vol (divset (D,n1)) > 0

then A646: 1 <= n1 by FINSEQ_3:25;

end;assume A645: n1 in dom D ; :: thesis: vol (divset (D,n1)) > 0

then A646: 1 <= n1 by FINSEQ_3:25;

per cases
( n1 = 1 or n1 > 1 )
by A646, XXREAL_0:1;

end;

suppose A647:
n1 = 1
; :: thesis: vol (divset (D,n1)) > 0

then A648:
upper_bound (divset (D,n1)) = D . n1
by A645, INTEGRA1:def 4;

lower_bound (divset (D,n1)) = lower_bound A by A645, A647, INTEGRA1:def 4;

then vol (divset (D,n1)) = (D . n1) - (lower_bound A) by A648, INTEGRA1:def 5;

hence vol (divset (D,n1)) > 0 by A628, A647, XREAL_1:50; :: thesis: verum

end;lower_bound (divset (D,n1)) = lower_bound A by A645, A647, INTEGRA1:def 4;

then vol (divset (D,n1)) = (D . n1) - (lower_bound A) by A648, INTEGRA1:def 5;

hence vol (divset (D,n1)) > 0 by A628, A647, XREAL_1:50; :: thesis: verum

suppose A649:
n1 > 1
; :: thesis: vol (divset (D,n1)) > 0

then A650:
upper_bound (divset (D,n1)) = D . n1
by A645, INTEGRA1:def 4;

lower_bound (divset (D,n1)) = D . (n1 - 1) by A645, A649, INTEGRA1:def 4;

then A651: vol (divset (D,n1)) = (D . n1) - (D . (n1 - 1)) by A650, INTEGRA1:def 5;

n1 < n1 + 1 by XREAL_1:29;

then A652: n1 - 1 < n1 by XREAL_1:19;

n1 - 1 in dom D by A645, A649, INTEGRA1:7;

then D . (n1 - 1) < D . n1 by A645, A652, SEQM_3:def 1;

hence vol (divset (D,n1)) > 0 by A651, XREAL_1:50; :: thesis: verum

end;lower_bound (divset (D,n1)) = D . (n1 - 1) by A645, A649, INTEGRA1:def 4;

then A651: vol (divset (D,n1)) = (D . n1) - (D . (n1 - 1)) by A650, INTEGRA1:def 5;

n1 < n1 + 1 by XREAL_1:29;

then A652: n1 - 1 < n1 by XREAL_1:19;

n1 - 1 in dom D by A645, A649, INTEGRA1:7;

then D . (n1 - 1) < D . n1 by A645, A652, SEQM_3:def 1;

hence vol (divset (D,n1)) > 0 by A651, XREAL_1:50; :: thesis: verum

1 <= k by A638, FINSEQ_3:25;

then 1 <= len v1 by A653, XXREAL_0:2;

then 1 in dom v1 by FINSEQ_3:25;

then A654: v1 . 1 in rng v1 by FUNCT_1:def 3;

rng v = rng v1 by A631, CLASSES1:75;

then consider n1 being Element of NAT such that

A655: n1 in dom v and

A656: v1 . 1 = v . n1 by A654, PARTFUN1:3;

n1 in Seg (len D) by A629, A655, FINSEQ_1:def 3;

then A657: n1 in dom D by FINSEQ_1:def 3;

v1 . 1 = H

.= vol (divset (D,n1)) ;

hence v1 . 1 > 0 by A644, A657; :: thesis: verum

proof

A676:
min ((v1 . k),(e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)))) <= v1 . k
by XXREAL_0:17;
A659:
k = 1

v1 . k in rng (upper_volume ((chi (A,A)),D))

min (rng (upper_volume ((chi (A,A)),D))) in rng (upper_volume ((chi (A,A)),D)) by XXREAL_2:def 7;

then consider m being Element of NAT such that

A669: m in dom (upper_volume ((chi (A,A)),D)) and

A670: min (rng (upper_volume ((chi (A,A)),D))) = (upper_volume ((chi (A,A)),D)) . m by PARTFUN1:3;

m in Seg (len (upper_volume ((chi (A,A)),D))) by A669, FINSEQ_1:def 3;

then A671: m in Seg (len D) by INTEGRA1:def 6;

then m in dom D by FINSEQ_1:def 3;

then A672: min (rng (upper_volume ((chi (A,A)),D))) = vol (divset (D,m)) by A670, INTEGRA1:20;

A673: v . m = H_{1}(m)
by A629, A632, A671

.= min (rng (upper_volume ((chi (A,A)),D))) by A672 ;

m in dom v by A629, A671, FINSEQ_1:def 3;

then min (rng (upper_volume ((chi (A,A)),D))) in rng v by A673, FUNCT_1:def 3;

then consider m1 being Element of NAT such that

A674: m1 in dom v1 and

A675: min (rng (upper_volume ((chi (A,A)),D))) = v1 . m1 by A662, PARTFUN1:3;

m1 >= 1 by A674, FINSEQ_3:25;

then v1 . 1 <= min (rng (upper_volume ((chi (A,A)),D))) by A638, A659, A674, A675, INTEGRA2:2;

hence v1 . k = min (rng (upper_volume ((chi (A,A)),D))) by A659, A668, XXREAL_0:1; :: thesis: verum

end;proof

A662:
rng v = rng v1
by A631, CLASSES1:75;
len v1 = len v
by A631, RFINSEQ:3;

then k in Seg (len v) by A638, FINSEQ_1:def 3;

then A660: 1 <= k by FINSEQ_1:1;

k in Seg (len v1) by A638, FINSEQ_1:def 3;

then k <= len v1 by FINSEQ_1:1;

then 1 <= len v1 by A660, XXREAL_0:2;

then A661: 1 in dom v1 by FINSEQ_3:25;

assume k <> 1 ; :: thesis: contradiction

then k > 1 by A660, XXREAL_0:1;

hence contradiction by A638, A643, A661; :: thesis: verum

end;then k in Seg (len v) by A638, FINSEQ_1:def 3;

then A660: 1 <= k by FINSEQ_1:1;

k in Seg (len v1) by A638, FINSEQ_1:def 3;

then k <= len v1 by FINSEQ_1:1;

then 1 <= len v1 by A660, XXREAL_0:2;

then A661: 1 in dom v1 by FINSEQ_3:25;

assume k <> 1 ; :: thesis: contradiction

then k > 1 by A660, XXREAL_0:1;

hence contradiction by A638, A643, A661; :: thesis: verum

v1 . k in rng (upper_volume ((chi (A,A)),D))

proof

then A668:
v1 . k >= min (rng (upper_volume ((chi (A,A)),D)))
by XXREAL_2:def 7;
v1 . k in rng v
by A638, A662, FUNCT_1:def 3;

then consider k2 being Element of NAT such that

A663: k2 in dom v and

A664: v1 . k = v . k2 by PARTFUN1:3;

A665: k2 in Seg (len D) by A629, A663, FINSEQ_1:def 3;

then A666: k2 in dom D by FINSEQ_1:def 3;

k2 in Seg (len (upper_volume ((chi (A,A)),D))) by A665, INTEGRA1:def 6;

then A667: k2 in dom (upper_volume ((chi (A,A)),D)) by FINSEQ_1:def 3;

v1 . k = H_{1}(k2)
by A629, A663, A664

.= vol (divset (D,k2)) ;

then v1 . k = (upper_volume ((chi (A,A)),D)) . k2 by A666, INTEGRA1:20;

hence v1 . k in rng (upper_volume ((chi (A,A)),D)) by A667, FUNCT_1:def 3; :: thesis: verum

end;then consider k2 being Element of NAT such that

A663: k2 in dom v and

A664: v1 . k = v . k2 by PARTFUN1:3;

A665: k2 in Seg (len D) by A629, A663, FINSEQ_1:def 3;

then A666: k2 in dom D by FINSEQ_1:def 3;

k2 in Seg (len (upper_volume ((chi (A,A)),D))) by A665, INTEGRA1:def 6;

then A667: k2 in dom (upper_volume ((chi (A,A)),D)) by FINSEQ_1:def 3;

v1 . k = H

.= vol (divset (D,k2)) ;

then v1 . k = (upper_volume ((chi (A,A)),D)) . k2 by A666, INTEGRA1:20;

hence v1 . k in rng (upper_volume ((chi (A,A)),D)) by A667, FUNCT_1:def 3; :: thesis: verum

min (rng (upper_volume ((chi (A,A)),D))) in rng (upper_volume ((chi (A,A)),D)) by XXREAL_2:def 7;

then consider m being Element of NAT such that

A669: m in dom (upper_volume ((chi (A,A)),D)) and

A670: min (rng (upper_volume ((chi (A,A)),D))) = (upper_volume ((chi (A,A)),D)) . m by PARTFUN1:3;

m in Seg (len (upper_volume ((chi (A,A)),D))) by A669, FINSEQ_1:def 3;

then A671: m in Seg (len D) by INTEGRA1:def 6;

then m in dom D by FINSEQ_1:def 3;

then A672: min (rng (upper_volume ((chi (A,A)),D))) = vol (divset (D,m)) by A670, INTEGRA1:20;

A673: v . m = H

.= min (rng (upper_volume ((chi (A,A)),D))) by A672 ;

m in dom v by A629, A671, FINSEQ_1:def 3;

then min (rng (upper_volume ((chi (A,A)),D))) in rng v by A673, FUNCT_1:def 3;

then consider m1 being Element of NAT such that

A674: m1 in dom v1 and

A675: min (rng (upper_volume ((chi (A,A)),D))) = v1 . m1 by A662, PARTFUN1:3;

m1 >= 1 by A674, FINSEQ_3:25;

then v1 . 1 <= min (rng (upper_volume ((chi (A,A)),D))) by A638, A659, A674, A675, INTEGRA2:2;

hence v1 . k = min (rng (upper_volume ((chi (A,A)),D))) by A659, A668, XXREAL_0:1; :: thesis: verum

set s = upper_integral f;

set sD = upper_sum (f,D);

let m be Nat; :: thesis: ( n <= m implies |.(((upper_sum (f,T)) . m) - (upper_integral f)).| < e )

reconsider mm = m as Element of NAT by ORDINAL1:def 12;

reconsider D1 = T . mm as Division of A ;

A677: delta D1 = (delta T) . m by Def2;

consider D2 being Division of A such that

A678: D <= D2 and

D1 <= D2 and

A679: rng D2 = (rng D1) \/ (rng D) and

0 <= (upper_sum (f,D)) - (upper_sum (f,D2)) and

0 <= (upper_sum (f,D1)) - (upper_sum (f,D2)) by A2;

set sD1 = upper_sum (f,(T . mm));

set sD2 = upper_sum (f,D2);

upper_sum (f,D2) <= upper_sum (f,D) by A1, A678, INTEGRA1:45;

then A680: (upper_sum (f,(T . mm))) - (upper_sum (f,D)) <= (upper_sum (f,(T . mm))) - (upper_sum (f,D2)) by XREAL_1:10;

(((upper_sum (f,D)) + (upper_sum (f,(T . mm)))) - (upper_sum (f,(T . mm)))) - (upper_integral f) < e / 2 by A576, A642, XREAL_1:19;

then (((upper_sum (f,(T . mm))) - (upper_integral f)) + (upper_sum (f,D))) - (upper_sum (f,(T . mm))) < e / 2 ;

then ((upper_sum (f,(T . mm))) - (upper_integral f)) + (upper_sum (f,D)) < (upper_sum (f,(T . mm))) + (e / 2) by XREAL_1:19;

then A681: (upper_sum (f,(T . mm))) - (upper_integral f) < ((upper_sum (f,(T . mm))) + (e / 2)) - (upper_sum (f,D)) by XREAL_1:20;

T . mm in divs A by INTEGRA1:def 3;

then A682: T . m in dom (upper_sum_set f) by FUNCT_2:def 1;

(upper_sum (f,T)) . m = upper_sum (f,(T . mm)) by INTEGRA2:def 2;

then (upper_sum (f,T)) . m = (upper_sum_set f) . (T . m) by INTEGRA1:def 10;

then (upper_sum (f,T)) . m in rng (upper_sum_set f) by A682, FUNCT_1:def 3;

then lower_bound (rng (upper_sum_set f)) <= (upper_sum (f,T)) . m by A574, SEQ_4:def 2;

then upper_integral f <= (upper_sum (f,T)) . m by INTEGRA1:def 14;

then A683: ((upper_sum (f,T)) . m) - (upper_integral f) >= 0 by XREAL_1:48;

(upper_bound (rng f)) - (lower_bound (rng f)) <= ((upper_bound (rng f)) - (lower_bound (rng f))) + 1 by XREAL_1:29;

then A684: (len D) * ((upper_bound (rng f)) - (lower_bound (rng f))) <= (len D) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1) by XREAL_1:64;

A685: min ((v1 . k),(e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)))) <= e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)) by XXREAL_0:17;

assume A686: n <= m ; :: thesis: |.(((upper_sum (f,T)) . m) - (upper_integral f)).| < e

then (delta T) . m < min ((v1 . k),(e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)))) by A641;

then (delta T) . m < e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)) by A685, XXREAL_0:2;

then ((delta T) . m) * ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)) < e by A630, A639, XREAL_1:79, XREAL_1:129;

then (((delta T) . m) * ((len D) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1))) * 2 < e ;

then A687: ((len D) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)) * ((delta T) . m) < e / 2 by XREAL_1:81;

(delta T) . m < min ((v1 . k),(e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)))) by A641, A686;

then delta D1 < v1 . k by A677, A676, XXREAL_0:2;

then ex D3 being Division of A st

( D <= D3 & D1 <= D3 & rng D3 = (rng D1) \/ (rng D) & (upper_sum (f,D1)) - (upper_sum (f,D3)) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) ) by A7, A658;

then A688: (upper_sum (f,D1)) - (upper_sum (f,D2)) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) by A679, Th6;

0 < (delta T) . m by A641, A686;

then ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * ((delta T) . m) <= ((len D) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)) * ((delta T) . m) by A684, XREAL_1:64;

then (upper_sum (f,(T . mm))) - (upper_sum (f,D2)) <= ((len D) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)) * ((delta T) . m) by A677, A688, XXREAL_0:2;

then (upper_sum (f,(T . mm))) - (upper_sum (f,D)) <= ((len D) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)) * ((delta T) . m) by A680, XXREAL_0:2;

then (upper_sum (f,(T . mm))) - (upper_sum (f,D)) < e / 2 by A687, XXREAL_0:2;

then ((upper_sum (f,(T . mm))) - (upper_sum (f,D))) + (e / 2) < (e / 2) + (e / 2) by XREAL_1:6;

then (upper_sum (f,(T . mm))) - (upper_integral f) < e by A681, XXREAL_0:2;

then ((upper_sum (f,T)) . m) - (upper_integral f) < e by INTEGRA2:def 2;

hence |.(((upper_sum (f,T)) . m) - (upper_integral f)).| < e by A683, ABSVALUE:def 1; :: thesis: verum

hence lim (upper_sum (f,T)) = upper_integral f by A571, SEQ_2:def 7; :: thesis: verum