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 () = 0 & ( for n being Element of NAT ex Tn being Division of A st
( Tn divide_into_equal n + 1 & T . n = Tn ) ) ) )

defpred S1[ set , set ] means ex n being Element of 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 () = 0 & ( for n being Element of NAT ex Tn being Division of A st
( Tn divide_into_equal n + 1 & T . n = Tn ) ) )

A2: for n being Element of NAT ex D being Element of divs A st S1[n,D]
proof
let n be Element of NAT ; :: thesis: ex D being Element of divs A st S1[n,D]
consider D being Division of A such that
A3: ( len D = n + 1 & ( for i being Nat st i in dom D holds
D . i = () + (((vol A) / (n + 1)) * i) ) ) by ;
reconsider D1 = D as Element of divs A by INTEGRA1:def 3;
take D1 ; :: thesis: S1[n,D1]
D divide_into_equal n + 1 by ;
hence S1[n,D1] ; :: thesis: verum
end;
consider T being sequence of (divs A) such that
A4: for n being Element of NAT holds S1[n,T . n] from reconsider T = T as DivSequence of A ;
A5: for n being Element of NAT ex Tn being Division of A st
( Tn divide_into_equal n + 1 & T . n = Tn )
proof
let n be Element of NAT ; :: thesis: ex Tn being Division of A st
( Tn divide_into_equal n + 1 & T . n = Tn )

ex n1 being Element of NAT ex Tn being Division of A st
( n1 = n & Tn = T . n & Tn divide_into_equal n1 + 1 ) by A4;
hence ex Tn being Division of A st
( Tn divide_into_equal n + 1 & T . n = Tn ) ; :: thesis: verum
end;
A6: for i being Element of NAT holds () . i = (vol A) / (i + 1)
proof
let i be Element of NAT ; :: thesis: () . i = (vol A) / (i + 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
A7: k in dom (upper_volume ((chi (A,A)),(T . i))) and
A8: (upper_volume ((chi (A,A)),(T . i))) . k = x1 by PARTFUN1:3;
k in Seg (len (upper_volume ((chi (A,A)),(T . i)))) by ;
then k in Seg (len D) by INTEGRA1:def 6;
then A9: k in dom D by FINSEQ_1:def 3;
A10: ex n being Element of NAT ex e being Division of A st
( n = i & e = D & e divide_into_equal n + 1 ) by A4;
A11: (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) = (vol A) / (i + 1)
proof
A12: now :: thesis: ( k = 1 implies (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) = (vol A) / (i + 1) )
A13: len D = i + 1 by ;
assume A14: k = 1 ; :: thesis: (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) = (vol A) / (i + 1)
then upper_bound (divset (D,k)) = D . 1 by ;
then upper_bound (divset (D,k)) = () + (((vol A) / (i + 1)) * 1) by ;
then (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) = (() + ((vol A) / (i + 1))) - () by ;
hence (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) = (vol A) / (i + 1) ; :: thesis: verum
end;
now :: thesis: ( k <> 1 implies (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) = (vol A) / (i + 1) )
assume A15: k <> 1 ; :: thesis: (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) = (vol A) / (i + 1)
then k - 1 in dom D by ;
then A16: D . (k - 1) = () + (((vol A) / (len D)) * (k - 1)) by ;
A17: D . k = () + (((vol A) / (len D)) * k) by ;
( lower_bound (divset (D,k)) = D . (k - 1) & upper_bound (divset (D,k)) = D . k ) by ;
hence (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) = (vol A) / (i + 1) by ; :: thesis: verum
end;
hence (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) = (vol A) / (i + 1) by A12; :: thesis: verum
end;
x1 = vol (divset (D,k)) by ;
hence x1 in {((vol A) / (i + 1))} by ; :: thesis: verum
end;
then A18: rng (upper_volume ((chi (A,A)),(T . i))) c= {((vol A) / (i + 1))} ;
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))) )
assume x1 in {((vol A) / (i + 1))} ; :: thesis: x1 in rng (upper_volume ((chi (A,A)),(T . i)))
then A19: x1 = (vol A) / (i + 1) by TARSKI:def 1;
A20: ex n being Element of NAT ex e being Division of A st
( n = i & e = D & e divide_into_equal n + 1 ) by A4;
rng D <> {} ;
then A21: 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)) = () + (((vol A) / (len D)) * 1) by ;
then A22: vol (divset (D,1)) = (() + ((vol A) / (len D))) - () by ;
1 in Seg (len D) by ;
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 A23: (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 ;
hence x1 in rng (upper_volume ((chi (A,A)),(T . i))) by ; :: thesis: verum
end;
then {((vol A) / (i + 1))} c= rng (upper_volume ((chi (A,A)),(T . i))) ;
then ( (delta T) . i = delta (T . i) & rng (upper_volume ((chi (A,A)),(T . i))) = {((vol A) / (i + 1))} ) by ;
then (delta T) . i in {((vol A) / (i + 1))} by XXREAL_2:def 8;
hence (delta T) . i = (vol A) / (i + 1) by TARSKI:def 1; :: thesis: verum
end;
A24: for a being Real st 0 < a holds
ex i being Element of NAT st |.((() . i) - 0).| < a
proof
let a be Real; :: thesis: ( 0 < a implies ex i being Element of NAT st |.((() . i) - 0).| < a )
A25: vol A >= 0 by INTEGRA1:9;
reconsider i1 = [\((vol A) / a)/] + 1 as Integer ;
assume A26: 0 < a ; :: thesis: ex i being Element of NAT st |.((() . i) - 0).| < a
then [\((vol A) / a)/] + 1 > 0 by ;
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 ;
then A27: (vol A) / (i1 + 1) < 1 * a by ;
A28: (delta T) . i1 = (vol A) / (i1 + 1) by A6;
((vol A) / (i1 + 1)) - 0 = |.(((vol A) / (i1 + 1)) - 0).| by ;
hence ex i being Element of NAT st |.((() . i) - 0).| < a by ; :: thesis: verum
end;
A29: for i, j being Element of NAT st i <= j holds
() . i >= () . j
proof
let i, j be Element of NAT ; :: thesis: ( i <= j implies () . i >= () . j )
assume i <= j ; :: thesis: () . i >= () . j
then A30: i + 1 <= j + 1 by XREAL_1:6;
vol A >= 0 by INTEGRA1:9;
then (vol A) / (i + 1) >= (vol A) / (j + 1) by ;
then (delta T) . i >= (vol A) / (j + 1) by A6;
hence (delta T) . i >= () . j by A6; :: thesis: verum
end;
A31: for a being Real st 0 < a holds
ex i being Nat st
for j being Nat st i <= j holds
|.((() . 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
|.((() . j) - 0).| < a )

assume A32: 0 < a ; :: thesis: ex i being Nat st
for j being Nat st i <= j holds
|.((() . j) - 0).| < a

consider i being Element of NAT such that
A33: |.((() . i) - 0).| < a by ;
(delta T) . i = delta (T . i) by INTEGRA3:def 2;
then (delta T) . i >= 0 by INTEGRA3:9;
then A34: (delta T) . i < a by ;
take i ; :: thesis: for j being Nat st i <= j holds
|.((() . j) - 0).| < a

let j be Nat; :: thesis: ( i <= j implies |.((() . j) - 0).| < a )
reconsider jj = j as Element of NAT by ORDINAL1:def 12;
assume i <= j ; :: thesis: |.((() . j) - 0).| < a
then (delta T) . jj <= () . i by A29;
then A35: (delta T) . j < a by ;
(delta T) . j = delta (T . jj) by INTEGRA3:def 2;
then (delta T) . j >= 0 by INTEGRA3:9;
hence |.((() . j) - 0).| < a by ; :: thesis: verum
end;
then A36: delta T is convergent by SEQ_2:def 6;
then lim () = 0 by ;
hence ex T being DivSequence of A st
( delta T is convergent & lim () = 0 & ( for n being Element of NAT ex Tn being Division of A st
( Tn divide_into_equal n + 1 & T . n = Tn ) ) ) by ; :: thesis: verum