let A be non empty closed_interval Subset of REAL; :: thesis: ( vol A > 0 implies ex T being DivSequence of A st
( delta T is convergent & lim (delta T) = 0 ) )
defpred S₁[ set , set ] means ex n being Nat ex e being Division of A st
( n = $1 & e = $2 & e divide_into_equal n + 1 );
assume A1: vol A > 0 ; :: thesis: ex T being DivSequence of A st
( delta T is convergent & lim (delta T) = 0 )
A2: for n being Element of NAT ex D being Element of divs A st S₁[n,D]

proof

let n be Element of NAT ; :: thesis: ex D being Element of divs A st S₁[n,D]
consider D being Division of A such that
A3: len D = n + 1 and
A4: for i being Nat st i in dom D holds
D . i = (lower_bound A) + (((vol A) / (n + 1)) * i) by A1, Lm4;
A5: D is Element of divs A by INTEGRA1:def 3;
D divide_into_equal n + 1 by A3, A4;
hence ex D being Element of divs A st S₁[n,D] by A5; :: thesis: verum

end;

consider T being sequence of (divs A) such that
A6: for n being Element of NAT holds S₁[n,T . n] from FUNCT_2:sch 3(A2);
reconsider T = T as DivSequence of A ;
A7: for i being Element of NAT holds (delta T) . i = (vol A) / (i + 1)

proof

let i be Element of NAT ; :: thesis: (delta T) . i = (vol A) / (i + 1)
(delta T) . i = delta (T . i) by INTEGRA3:def 2;
then A8: (delta T) . i = max (rng (upper_volume ((chi (A,A)),(T . i)))) by INTEGRA3:def 1;
for x1 being object st x1 in rng (upper_volume ((chi (A,A)),(T . i))) holds
x1 in {((vol A) / (i + 1))}

proof

reconsider D = T . i as Division of A ;
let x1 be object ; :: thesis: ( x1 in rng (upper_volume ((chi (A,A)),(T . i))) implies x1 in {((vol A) / (i + 1))} )
assume x1 in rng (upper_volume ((chi (A,A)),(T . i))) ; :: thesis: x1 in {((vol A) / (i + 1))}
then consider k being Element of NAT such that
A9: k in dom (upper_volume ((chi (A,A)),(T . i))) and
A10: (upper_volume ((chi (A,A)),(T . i))) . k = x1 by PARTFUN1:3;
A11: ex n being Nat ex e being Division of A st
( n = i & e = D & e divide_into_equal n + 1 ) by A6;
k in Seg (len (upper_volume ((chi (A,A)),(T . i)))) by A9, FINSEQ_1:def 3;
then A12: k in Seg (len D) by INTEGRA1:def 6;
A13: (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) = (vol A) / (i + 1)

proof

A14: 1 <= k by A9, FINSEQ_3:25;

now :: thesis: (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) = (vol A) / (i + 1)

per cases ( k = 1 or k > 1 ) by A14, XXREAL_0:1;

suppose A15: k = 1 ; :: thesis: (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) = (vol A) / (i + 1)

A16: 1 in dom D by A12, A15, FINSEQ_1:def 3;
then upper_bound (divset (D,k)) = D . 1 by A15, INTEGRA1:def 4;
then upper_bound (divset (D,k)) = (lower_bound A) + (((vol A) / (i + 1)) * 1) by A11, A16;
then (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) = ((lower_bound A) + ((vol A) / (i + 1))) - (lower_bound A) by A15, A16, INTEGRA1:def 4
.= ((vol A) / (i + 1)) - ((lower_bound A) - (lower_bound A)) ;
hence (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) = (vol A) / (i + 1) ; :: thesis: verum

end;

suppose A17: k > 1 ; :: thesis: (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) = (vol A) / (i + 1)

A18: k in dom D by A12, FINSEQ_1:def 3;
then A19: lower_bound (divset (D,k)) = D . (k - 1) by A17, INTEGRA1:def 4;
k - 1 in dom D by A17, A18, INTEGRA1:7;
then A20: D . (k - 1) = (lower_bound A) + (((vol A) / (len D)) * (k - 1)) by A11;
A21: upper_bound (divset (D,k)) = D . k by A17, A18, INTEGRA1:def 4;
D . k = (lower_bound A) + (((vol A) / (len D)) * k) by A11, A18;
hence (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) = (vol A) / (i + 1) by A11, A19, A21, A20; :: thesis: verum

end;

end;

end;

hence (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) = (vol A) / (i + 1) ; :: thesis: verum

end;

k in dom D by A12, FINSEQ_1:def 3;
then x1 = vol (divset (D,k)) by A10, INTEGRA1:20;
then x1 = (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) by INTEGRA1:def 5;
hence x1 in {((vol A) / (i + 1))} by A13, TARSKI:def 1; :: thesis: verum

end;

then A22: rng (upper_volume ((chi (A,A)),(T . i))) c= {((vol A) / (i + 1))} by TARSKI:def 3;
for x1 being object st x1 in {((vol A) / (i + 1))} holds
x1 in rng (upper_volume ((chi (A,A)),(T . i)))

proof

reconsider D = T . i as Division of A ;
let x1 be object ; :: thesis: ( x1 in {((vol A) / (i + 1))} implies x1 in rng (upper_volume ((chi (A,A)),(T . i))) )
A23: vol (divset (D,1)) = (upper_bound (divset (D,1))) - (lower_bound (divset (D,1))) by INTEGRA1:def 5;
A24: ex n being Nat ex e being Division of A st
( n = i & e = D & e divide_into_equal n + 1 ) by A6;
rng D <> {} ;
then A25: 1 in dom D by FINSEQ_3:32;
then upper_bound (divset (D,1)) = D . 1 by INTEGRA1:def 4;
then upper_bound (divset (D,1)) = (lower_bound A) + (((vol A) / (len D)) * 1) by A25, A24;
then A26: vol (divset (D,1)) = ((lower_bound A) + ((vol A) / (len D))) - (lower_bound A) by A25, A23, INTEGRA1:def 4
.= (vol A) / (len D) ;
assume x1 in {((vol A) / (i + 1))} ; :: thesis: x1 in rng (upper_volume ((chi (A,A)),(T . i)))
then A27: x1 = (vol A) / (i + 1) by TARSKI:def 1;
1 in Seg (len D) by A25, FINSEQ_1:def 3;
then 1 in Seg (len (upper_volume ((chi (A,A)),D))) by INTEGRA1:def 6;
then 1 in dom (upper_volume ((chi (A,A)),D)) by FINSEQ_1:def 3;
then A28: (upper_volume ((chi (A,A)),D)) . 1 in rng (upper_volume ((chi (A,A)),D)) by FUNCT_1:def 3;
(upper_volume ((chi (A,A)),D)) . 1 = vol (divset (D,1)) by A25, INTEGRA1:20;
hence x1 in rng (upper_volume ((chi (A,A)),(T . i))) by A27, A28, A24, A26; :: thesis: verum

end;

then {((vol A) / (i + 1))} c= rng (upper_volume ((chi (A,A)),(T . i))) by TARSKI:def 3;
then rng (upper_volume ((chi (A,A)),(T . i))) = {((vol A) / (i + 1))} by A22, XBOOLE_0:def 10;
then (delta T) . i in {((vol A) / (i + 1))} by A8, XXREAL_2:def 8;
hence (delta T) . i = (vol A) / (i + 1) by TARSKI:def 1; :: thesis: verum

end;

A29: for a being Real st 0 < a holds
ex i being Nat st |.(((delta T) . i) - 0).| < a

proof

let a be Real; :: thesis: ( 0 < a implies ex i being Nat st |.(((delta T) . i) - 0).| < a )
A30: vol A >= 0 by INTEGRA1:9;
reconsider i1 = [\((vol A) / a)/] + 1 as Integer ;
assume A31: 0 < a ; :: thesis: ex i being Nat st |.(((delta T) . i) - 0).| < a
then [\((vol A) / a)/] + 1 > 0 by A30, INT_1:29;
then reconsider i1 = i1 as Element of NAT by INT_1:3;
i1 < i1 + 1 by NAT_1:13;
then (vol A) / a < 1 * (i1 + 1) by INT_1:29, XXREAL_0:2;
then A32: (vol A) / (i1 + 1) < 1 * a by A31, XREAL_1:113;
A33: (delta T) . i1 = (vol A) / (i1 + 1) by A7;
((vol A) / (i1 + 1)) - 0 = |.(((vol A) / (i1 + 1)) - 0).| by A30, ABSVALUE:def 1;
hence ex i being Nat st |.(((delta T) . i) - 0).| < a by A32, A33; :: thesis: verum

end;

A34: for i being Nat holds (delta T) . i >= 0

proof

let i be Nat; :: thesis: (delta T) . i >= 0
reconsider ii = i as Element of NAT by ORDINAL1:def 12;
(delta T) . i = delta (T . ii) by INTEGRA3:def 2;
hence (delta T) . i >= 0 by INTEGRA3:9; :: thesis: verum

end;

A35: for i, j being Nat st i <= j holds
(delta T) . i >= (delta T) . j

proof

let i, j be Nat; :: thesis: ( i <= j implies (delta T) . i >= (delta T) . j )
assume i <= j ; :: thesis: (delta T) . i >= (delta T) . j
then A36: i + 1 <= j + 1 by XREAL_1:6;
A37: ( i in NAT & j in NAT ) by ORDINAL1:def 12;
vol A >= 0 by INTEGRA1:9;
then (vol A) / (i + 1) >= (vol A) / (j + 1) by A36, XREAL_1:118;
then (delta T) . i >= (vol A) / (j + 1) by A7, A37;
hence (delta T) . i >= (delta T) . j by A7, A37; :: thesis: verum

end;

A38: for a being Real st 0 < a holds
ex i being Nat st
for j being Nat st i <= j holds
|.(((delta T) . j) - 0).| < a

proof

let a be Real; :: thesis: ( 0 < a implies ex i being Nat st
for j being Nat st i <= j holds
|.(((delta T) . j) - 0).| < a )
assume A39: 0 < a ; :: thesis: ex i being Nat st
for j being Nat st i <= j holds
|.(((delta T) . j) - 0).| < a
consider i being Nat such that
A40: |.(((delta T) . i) - 0).| < a by A29, A39;
(delta T) . i >= 0 by A34;
then A41: (delta T) . i < a by A40, ABSVALUE:def 1;
for j being Nat st i <= j holds
|.(((delta T) . j) - 0).| < a

proof

let j be Nat; :: thesis: ( i <= j implies |.(((delta T) . j) - 0).| < a )
assume i <= j ; :: thesis: |.(((delta T) . j) - 0).| < a
then (delta T) . j <= (delta T) . i by A35;
then A42: (delta T) . j < a by A41, XXREAL_0:2;
(delta T) . j >= 0 by A34;
hence |.(((delta T) . j) - 0).| < a by A42, ABSVALUE:def 1; :: thesis: verum

end;

hence ex i being Nat st
for j being Nat st i <= j holds
|.(((delta T) . j) - 0).| < a ; :: thesis: verum

end;

then A43: delta T is convergent by SEQ_2:def 6;
then lim (delta T) = 0 by A38, SEQ_2:def 7;
hence ex T being DivSequence of A st
( delta T is convergent & lim (delta T) = 0 ) by A43; :: thesis: verum