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 )

proof

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;

A562: for e being Real st e > 0 holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((lower_sum (f,T)) . m) - (lower_integral f)).| < e

proof

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₁( 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₁(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₁[ 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₁[k]

proof

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₁(k) by A571, A578, A573, A576;
then v . k > 0 by A577;
then S₁[Hk] by A571, A573, A575, A576, A578, FUNCT_1:11, FUNCT_1:12;
hence ex k being Nat st S₁[k] ; :: thesis: verum

end;

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

proof

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;

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;

end;

end;

then consider n being Nat such that
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

A585: 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: ( 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;

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

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;

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;

end;

end;

A594: k <= len v1 by A579, FINSEQ_3:25;
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₁(n1) by A571, A596, A597
.= vol (divset (D,n1)) ;
hence v1 . 1 > 0 by A585, A598; :: thesis: verum

end;

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

proof

A600: k = 1

proof

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;

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

(upper_bound (rng f)) - (lower_bound (rng f)) <= ((upper_bound (rng f)) - (lower_bound (rng f))) + 1 by XREAL_1:29;
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;

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