let A be non empty closed_interval Subset of REAL; :: thesis:
let f be Function of A,REAL; :: thesis:
let T be DivSequence of A; :: thesis:
assume A1: f | A is bounded ; :: thesis:
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:
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:
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

let e be Real; :: thesis:
assume e > 0 ; :: thesis:
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:
let m be Nat; :: thesis:
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
assume n <= m ; :: thesis:
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:

end;

A571: for e being Real st e > 0 holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((upper_sum (f,T)) . m) - (upper_integral f)).| < e

proof

let e be Real; :: thesis:
assume A572: e > 0 ; :: thesis:
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

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;

per cases ;

suppose A581: D3 . 1 <> lower_bound A ; :: thesis:

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:

end;

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 )

proof

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

proof

let i be Nat; :: thesis:
assume that
A599: 1 <= i and
A600: i <= len (mid ((upper_volume (f,D3)),2,(len (upper_volume (f,D3))))) ; :: thesis:
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

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;

per cases ;

suppose A611: i = 1 ; :: thesis:

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:

end;

suppose A614: i <> 1 ; :: thesis:

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:

end;

end;

end;

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 ) ; :: thesis:

end;

then consider D being Division of A such that
D in dom (upper_sum_set f) and
A627: y = (upper_sum_set f) . D and
A628: D . 1 > lower_bound A ;
deffunc H₁( 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₁(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₁[ 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₁[k]

proof

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₁(k) by A629, A632, A635, A637;
then v . k > 0 by A636;
then S₁[Hk] by A632, A634, A635, A637, FUNCT_1:11, FUNCT_1:12;
hence ex k being Nat st S₁[k] ; :: thesis:

end;

consider k being Nat such that
A638: ( S₁[k] & ( for n being Nat st S₁[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

proof

per cases by XXREAL_0:15;

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

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

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:

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:

end;

then consider n being Nat such that
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:
A642: y = upper_sum (f,D) by A627, INTEGRA1:def 10;
A643: v1 . 1 > 0

proof

A644: for n1 being Element of NAT st n1 in dom D holds
vol (divset (D,n1)) > 0

proof

let n1 be Element of NAT ; :: thesis:
assume A645: n1 in dom D ; :: thesis:
then A646: 1 <= n1 by FINSEQ_3:25;

per cases by A646, XXREAL_0:1;

suppose A647: n1 = 1 ; :: thesis:

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:

end;

suppose A649: n1 > 1 ; :: thesis:

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:

end;

A653: k <= len v1 by A638, FINSEQ_3:25;
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₁(n1) by A629, A655, A656
.= vol (divset (D,n1)) ;
hence v1 . 1 > 0 by A644, A657; :: thesis:

end;

A658: v1 . k = min (rng (upper_volume ((chi (A,A)),D)))

proof

A659: k = 1

proof

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:
then k > 1 by A660, XXREAL_0:1;
hence contradiction by A638, A643, A661; :: thesis:

end;

A662: rng v = rng v1 by A631, CLASSES1:75;
v1 . k in rng (upper_volume ((chi (A,A)),D))

proof

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₁(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:

end;

end;

end;

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