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

( lower_sum (f,T) is convergent & lim (lower_sum (f,T)) = lower_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

( lower_sum (f,T) is convergent & lim (lower_sum (f,T)) = lower_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 ( lower_sum (f,T) is convergent & lim (lower_sum (f,T)) = lower_integral f ) )

assume that

A1: f | A is bounded and

A2: ( delta T is 0 -convergent & delta T is non-zero ) and

A3: vol A <> 0 ; :: thesis: ( lower_sum (f,T) is convergent & lim (lower_sum (f,T)) = lower_integral f )

A4: delta T is convergent by A2, FDIFF_1:def 1;

A5: 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 <= (lower_sum (f,D2)) - (lower_sum (f,D)) & 0 <= (lower_sum (f,D2)) - (lower_sum (f,D1)) ) by A1, Th20;

A10: 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) & (lower_sum (f,D2)) - (lower_sum (f,D1)) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) ) by A1, Th21;

A552: lim (delta T) = 0 by A2, FDIFF_1:def 1;

A553: delta T is non-zero by A2;

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

|.(((lower_sum (f,T)) . m) - (lower_integral f)).| < e

hence lim (lower_sum (f,T)) = lower_integral f by A562, 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

( lower_sum (f,T) is convergent & lim (lower_sum (f,T)) = lower_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

( lower_sum (f,T) is convergent & lim (lower_sum (f,T)) = lower_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 ( lower_sum (f,T) is convergent & lim (lower_sum (f,T)) = lower_integral f ) )

assume that

A1: f | A is bounded and

A2: ( delta T is 0 -convergent & delta T is non-zero ) and

A3: vol A <> 0 ; :: thesis: ( lower_sum (f,T) is convergent & lim (lower_sum (f,T)) = lower_integral f )

A4: delta T is convergent by A2, FDIFF_1:def 1;

A5: 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 <= (lower_sum (f,D2)) - (lower_sum (f,D)) & 0 <= (lower_sum (f,D2)) - (lower_sum (f,D1)) ) by A1, Th20;

A10: 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) & (lower_sum (f,D2)) - (lower_sum (f,D1)) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) ) by A1, Th21;

A552: lim (delta T) = 0 by A2, FDIFF_1:def 1;

A553: delta T is non-zero by A2;

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

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

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

|.(((delta T) . m) - 0).| < e by A4, A552, 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;

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

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

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

consider D being Division of A such that

A559: D = T . mm ;

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

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

then i in dom D by FINSEQ_1:def 3;

then A560: delta (T . mm) = vol (divset ((T . mm),i)) by A558, A559, INTEGRA1:20;

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

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

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

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

hence ( 0 < (delta T) . m & (delta T) . m < e ) by A561, A556, A560, 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

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

|.(((delta T) . m) - 0).| < e by A4, A552, 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;

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

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

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

consider D being Division of A such that

A559: D = T . mm ;

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

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

then i in dom D by FINSEQ_1:def 3;

then A560: delta (T . mm) = vol (divset ((T . mm),i)) by A558, A559, INTEGRA1:20;

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

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

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

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

hence ( 0 < (delta T) . m & (delta T) . m < e ) by A561, A556, A560, INTEGRA1:9, XREAL_1:6; :: thesis: verum

ex n being Nat st

for m being Nat st n <= m holds

|.(((lower_sum (f,T)) . m) - (lower_integral f)).| < e

proof

hence
lower_sum (f,T) is convergent
by SEQ_2:def 6; :: thesis: lim (lower_sum (f,T)) = lower_integral f
set h = lower_bound (rng f);

set H = upper_bound (rng f);

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

for m being Nat st n <= m holds

|.(((lower_sum (f,T)) . m) - (lower_integral f)).| < e )

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

for m being Nat st n <= m holds

|.(((lower_sum (f,T)) . m) - (lower_integral f)).| < e

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

reconsider e = e as Real ;

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

A566: rng (lower_sum_set f) is bounded_above by A1, INTEGRA2:36;

lower_integral f = upper_bound (rng (lower_sum_set f)) by INTEGRA1:def 15;

then consider y being Real such that

A567: y in rng (lower_sum_set f) and

A568: (lower_integral f) - (e / 2) < y by A564, A566, SEQ_4:def 1;

consider D being Division of A such that

D in dom (lower_sum_set f) and

A569: y = (lower_sum_set f) . D and

A570: D . 1 > lower_bound A by A3, A567, Lm7;

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

set p = len D;

consider v being FinSequence of REAL such that

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

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

consider v1 being non-decreasing FinSequence of REAL such that

A572: v,v1 are_fiberwise_equipotent by INTEGRA2:3;

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

A573: dom v = Seg (len D) by A571, FINSEQ_1:def 3;

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

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

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

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

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

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

A582: 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 A554;

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

|.(((lower_sum (f,T)) . m) - (lower_integral f)).| < e

A583: y = lower_sum (f,D) by A569, INTEGRA1:def 11;

A584: v1 . 1 > 0

then A617: (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;

set sD = lower_sum (f,D);

set s = lower_integral f;

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

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

reconsider D1 = T . mm as Division of A ;

A618: 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 A619: n <= m ; :: thesis: |.(((lower_sum (f,T)) . m) - (lower_integral f)).| < e

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

then A620: delta D1 < min ((v1 . k),(e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)))) by Def2;

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

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

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

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

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

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

then A622: T . mm in dom (lower_sum_set f) by FUNCT_2:def 1;

(lower_sum (f,T)) . mm = lower_sum (f,(T . mm)) by INTEGRA2:def 3;

then (lower_sum (f,T)) . m = (lower_sum_set f) . (T . m) by INTEGRA1:def 11;

then (lower_sum (f,T)) . m in rng (lower_sum_set f) by A622, FUNCT_1:def 3;

then upper_bound (rng (lower_sum_set f)) >= (lower_sum (f,T)) . m by A566, SEQ_4:def 1;

then lower_integral f >= (lower_sum (f,T)) . m by INTEGRA1:def 15;

then A623: (lower_integral f) - ((lower_sum (f,T)) . m) >= 0 by XREAL_1:48;

0 < (delta T) . m by A582, A619;

then A624: ((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 A617, XREAL_1:64;

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

consider D2 being Division of A such that

A625: D <= D2 and

D1 <= D2 and

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

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

0 <= (lower_sum (f,D2)) - (lower_sum (f,D1)) by A5;

set sD2 = lower_sum (f,D2);

A627: ((lower_sum (f,D)) - (lower_sum (f,(T . mm)))) - ((lower_sum (f,D2)) - (lower_sum (f,(T . mm)))) = (lower_sum (f,D)) - (lower_sum (f,D2)) ;

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

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

then ex D3 being Division of A st

( D <= D3 & D1 <= D3 & rng D3 = (rng D1) \/ (rng D) & (lower_sum (f,D3)) - (lower_sum (f,D1)) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) ) by A10, A599;

then A628: (lower_sum (f,D2)) - (lower_sum (f,D1)) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) by A626, Th6;

(lower_sum (f,D)) - (lower_sum (f,D2)) <= 0 by A1, A625, INTEGRA1:46, XREAL_1:47;

then A629: (lower_sum (f,D)) - (lower_sum (f,(T . mm))) <= (lower_sum (f,D2)) - (lower_sum (f,(T . mm))) by A627, XREAL_1:50;

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

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

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

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

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

((lower_integral f) - (lower_sum (f,(T . mm)))) + (lower_sum (f,(T . mm))) < (lower_sum (f,D)) + (e / 2) by A568, A583, XREAL_1:19;

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

then (lower_integral f) - (lower_sum (f,(T . mm))) < e by A630, XXREAL_0:2;

then (lower_integral f) - ((lower_sum (f,T)) . m) < e by INTEGRA2:def 3;

then |.((lower_integral f) - ((lower_sum (f,T)) . m)).| < e by A623, ABSVALUE:def 1;

then |.(- ((lower_integral f) - ((lower_sum (f,T)) . m))).| < e by COMPLEX1:52;

hence |.(((lower_sum (f,T)) . m) - (lower_integral f)).| < e ; :: thesis: verum

end;set H = upper_bound (rng f);

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

for m being Nat st n <= m holds

|.(((lower_sum (f,T)) . m) - (lower_integral f)).| < e )

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

for m being Nat st n <= m holds

|.(((lower_sum (f,T)) . m) - (lower_integral f)).| < e

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

reconsider e = e as Real ;

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

A566: rng (lower_sum_set f) is bounded_above by A1, INTEGRA2:36;

lower_integral f = upper_bound (rng (lower_sum_set f)) by INTEGRA1:def 15;

then consider y being Real such that

A567: y in rng (lower_sum_set f) and

A568: (lower_integral f) - (e / 2) < y by A564, A566, SEQ_4:def 1;

consider D being Division of A such that

D in dom (lower_sum_set f) and

A569: y = (lower_sum_set f) . D and

A570: D . 1 > lower_bound A by A3, A567, Lm7;

deffunc H

set p = len D;

consider v being FinSequence of REAL such that

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

v . j = H

consider v1 being non-decreasing FinSequence of REAL such that

A572: v,v1 are_fiberwise_equipotent by INTEGRA2:3;

defpred S

A573: dom v = Seg (len D) by A571, FINSEQ_1:def 3;

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

A575: v = v1 * H by A572, CLASSES1:77;

consider k being Element of NAT such that

A576: k in dom D and

A577: vol (divset (D,k)) > 0 by A3, Th2;

A578: dom D = Seg (len v) by A571, FINSEQ_1:def 3;

then H . k in dom v1 by A571, A573, A575, A576, FUNCT_1:11;

then reconsider Hk = H . k as Nat ;

v . k = H_{1}(k)
by A571, A578, A573, A576;

then v . k > 0 by A577;

then S_{1}[Hk]
by A571, A573, A575, A576, A578, 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

A575: v = v1 * H by A572, CLASSES1:77;

consider k being Element of NAT such that

A576: k in dom D and

A577: vol (divset (D,k)) > 0 by A3, Th2;

A578: dom D = Seg (len v) by A571, FINSEQ_1:def 3;

then H . k in dom v1 by A571, A573, A575, A576, FUNCT_1:11;

then reconsider Hk = H . k as Nat ;

v . k = H

then v . k > 0 by A577;

then S

hence ex k being Nat st S

A579: ( S

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

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

then A581: (2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1) > 0 by A565, 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 A579; :: 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 A563, A581, XREAL_1:139; :: thesis: verum

end;A582: 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 A554;

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

|.(((lower_sum (f,T)) . m) - (lower_integral f)).| < e

A583: y = lower_sum (f,D) by A569, INTEGRA1:def 11;

A584: v1 . 1 > 0

proof

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

vol (divset (D,n1)) > 0

1 <= k by A579, FINSEQ_3:25;

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

then 1 in dom v1 by FINSEQ_3:25;

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

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

then consider n1 being Element of NAT such that

A596: n1 in dom v and

A597: v1 . 1 = v . n1 by A595, PARTFUN1:3;

n1 in Seg (len D) by A571, A596, FINSEQ_1:def 3;

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

v1 . 1 = H_{1}(n1)
by A571, A596, A597

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

hence v1 . 1 > 0 by A585, A598; :: thesis: verum

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

proof

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

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

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

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

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

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

end;

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

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

lower_bound (divset (D,n1)) = lower_bound A by A586, A588, INTEGRA1:def 4;

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

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

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

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

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

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

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

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

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

n1 < n1 + 1 by XREAL_1:29;

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

n1 - 1 in dom D by A586, A590, INTEGRA1:7;

then D . (n1 - 1) < D . n1 by A586, A593, SEQM_3:def 1;

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

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

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

n1 < n1 + 1 by XREAL_1:29;

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

n1 - 1 in dom D by A586, A590, INTEGRA1:7;

then D . (n1 - 1) < D . n1 by A586, A593, SEQM_3:def 1;

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

1 <= k by A579, FINSEQ_3:25;

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

then 1 in dom v1 by FINSEQ_3:25;

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

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

then consider n1 being Element of NAT such that

A596: n1 in dom v and

A597: v1 . 1 = v . n1 by A595, PARTFUN1:3;

n1 in Seg (len D) by A571, A596, FINSEQ_1:def 3;

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

v1 . 1 = H

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

hence v1 . 1 > 0 by A585, A598; :: thesis: verum

proof

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

then consider m being Element of NAT such that

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

A604: 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 A603, FINSEQ_1:def 3;

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

then m in dom D by FINSEQ_1:def 3;

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

A607: v . m = H_{1}(m)
by A571, A573, A605

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

A608: rng v = rng v1 by A572, CLASSES1:75;

m in dom v by A571, A605, FINSEQ_1:def 3;

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

then consider m1 being Element of NAT such that

A609: m1 in dom v1 and

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

v1 . k in rng v1 by A579, FUNCT_1:def 3;

then consider k2 being Element of NAT such that

A611: k2 in dom v and

A612: v1 . k = v . k2 by A608, PARTFUN1:3;

A613: k2 in Seg (len D) by A571, A611, FINSEQ_1:def 3;

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

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

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

v1 . k = H_{1}(k2)
by A571, A611, A612

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

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

then v1 . k in rng (upper_volume ((chi (A,A)),D)) by A615, FUNCT_1:def 3;

then A616: v1 . k >= min (rng (upper_volume ((chi (A,A)),D))) by XXREAL_2:def 7;

m1 >= 1 by A609, FINSEQ_3:25;

then v1 . 1 <= min (rng (upper_volume ((chi (A,A)),D))) by A579, A600, A609, A610, INTEGRA2:2;

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

end;proof

min (rng (upper_volume ((chi (A,A)),D))) in rng (upper_volume ((chi (A,A)),D))
by XXREAL_2:def 7;
len v1 = len v
by A572, RFINSEQ:3;

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

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

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

then k <= len v1 by FINSEQ_1:1;

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

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

assume k <> 1 ; :: thesis: contradiction

then k > 1 by A601, XXREAL_0:1;

hence contradiction by A579, A584, A602; :: thesis: verum

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

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

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

then k <= len v1 by FINSEQ_1:1;

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

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

assume k <> 1 ; :: thesis: contradiction

then k > 1 by A601, XXREAL_0:1;

hence contradiction by A579, A584, A602; :: thesis: verum

then consider m being Element of NAT such that

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

A604: 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 A603, FINSEQ_1:def 3;

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

then m in dom D by FINSEQ_1:def 3;

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

A607: v . m = H

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

A608: rng v = rng v1 by A572, CLASSES1:75;

m in dom v by A571, A605, FINSEQ_1:def 3;

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

then consider m1 being Element of NAT such that

A609: m1 in dom v1 and

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

v1 . k in rng v1 by A579, FUNCT_1:def 3;

then consider k2 being Element of NAT such that

A611: k2 in dom v and

A612: v1 . k = v . k2 by A608, PARTFUN1:3;

A613: k2 in Seg (len D) by A571, A611, FINSEQ_1:def 3;

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

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

then A615: 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 A614, INTEGRA1:20;

then v1 . k in rng (upper_volume ((chi (A,A)),D)) by A615, FUNCT_1:def 3;

then A616: v1 . k >= min (rng (upper_volume ((chi (A,A)),D))) by XXREAL_2:def 7;

m1 >= 1 by A609, FINSEQ_3:25;

then v1 . 1 <= min (rng (upper_volume ((chi (A,A)),D))) by A579, A600, A609, A610, INTEGRA2:2;

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

then A617: (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;

set sD = lower_sum (f,D);

set s = lower_integral f;

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

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

reconsider D1 = T . mm as Division of A ;

A618: 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 A619: n <= m ; :: thesis: |.(((lower_sum (f,T)) . m) - (lower_integral f)).| < e

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

then A620: delta D1 < min ((v1 . k),(e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)))) by Def2;

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

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

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

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

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

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

then A622: T . mm in dom (lower_sum_set f) by FUNCT_2:def 1;

(lower_sum (f,T)) . mm = lower_sum (f,(T . mm)) by INTEGRA2:def 3;

then (lower_sum (f,T)) . m = (lower_sum_set f) . (T . m) by INTEGRA1:def 11;

then (lower_sum (f,T)) . m in rng (lower_sum_set f) by A622, FUNCT_1:def 3;

then upper_bound (rng (lower_sum_set f)) >= (lower_sum (f,T)) . m by A566, SEQ_4:def 1;

then lower_integral f >= (lower_sum (f,T)) . m by INTEGRA1:def 15;

then A623: (lower_integral f) - ((lower_sum (f,T)) . m) >= 0 by XREAL_1:48;

0 < (delta T) . m by A582, A619;

then A624: ((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 A617, XREAL_1:64;

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

consider D2 being Division of A such that

A625: D <= D2 and

D1 <= D2 and

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

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

0 <= (lower_sum (f,D2)) - (lower_sum (f,D1)) by A5;

set sD2 = lower_sum (f,D2);

A627: ((lower_sum (f,D)) - (lower_sum (f,(T . mm)))) - ((lower_sum (f,D2)) - (lower_sum (f,(T . mm)))) = (lower_sum (f,D)) - (lower_sum (f,D2)) ;

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

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

then ex D3 being Division of A st

( D <= D3 & D1 <= D3 & rng D3 = (rng D1) \/ (rng D) & (lower_sum (f,D3)) - (lower_sum (f,D1)) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) ) by A10, A599;

then A628: (lower_sum (f,D2)) - (lower_sum (f,D1)) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) by A626, Th6;

(lower_sum (f,D)) - (lower_sum (f,D2)) <= 0 by A1, A625, INTEGRA1:46, XREAL_1:47;

then A629: (lower_sum (f,D)) - (lower_sum (f,(T . mm))) <= (lower_sum (f,D2)) - (lower_sum (f,(T . mm))) by A627, XREAL_1:50;

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

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

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

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

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

((lower_integral f) - (lower_sum (f,(T . mm)))) + (lower_sum (f,(T . mm))) < (lower_sum (f,D)) + (e / 2) by A568, A583, XREAL_1:19;

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

then (lower_integral f) - (lower_sum (f,(T . mm))) < e by A630, XXREAL_0:2;

then (lower_integral f) - ((lower_sum (f,T)) . m) < e by INTEGRA2:def 3;

then |.((lower_integral f) - ((lower_sum (f,T)) . m)).| < e by A623, ABSVALUE:def 1;

then |.(- ((lower_integral f) - ((lower_sum (f,T)) . m))).| < e by COMPLEX1:52;

hence |.(((lower_sum (f,T)) . m) - (lower_integral f)).| < e ; :: thesis: verum

hence lim (lower_sum (f,T)) = lower_integral f by A562, SEQ_2:def 7; :: thesis: verum