let A be 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 & ( for n being Element of NAT ex Tn being Division of A st
( Tn divide_into_equal n + 1 & T . n = Tn ) ) ) )
assume A1: vol A > 0 ; :: thesis: ex T being DivSequence of A st
( delta T is convergent & lim (delta T) = 0 & ( for n being Element of NAT ex Tn being Division of A st
( Tn divide_into_equal n + 1 & T . n = Tn ) ) )
defpred S₁[ 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 );
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 & ( for i being Element of NAT st i in dom D holds
D . i = (inf A) + (((vol A) / (n + 1)) * i) ) ) by A1, Th15;
reconsider D1 = D as Element of divs A by INTEGRA1:def 3;
take D1 ; :: thesis: S₁[n,D1]
D divide_into_equal n + 1 by A3, INTEGRA4:def 1;
hence S₁[n,D1] ; :: thesis: verum

end;

consider T being Function of NAT ,(divs A) such that
A4: for n being Element of NAT holds S₁[n,T . n] from FUNCT_2:sch 3(A2);
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 (delta T) . i = (vol A) / (i + 1)

proof

let i be Element of NAT ; :: thesis: (delta T) . i = (vol A) / (i + 1)
A7: (delta T) . i = delta (T . i) by INTEGRA2:def 3;
rng (upper_volume (chi A,A),(T . i)) = {((vol A) / (i + 1))}

proof

for x1 being set st x1 in rng (upper_volume (chi A,A),(T . i)) holds
x1 in {((vol A) / (i + 1))}

proof

let x1 be set ; :: 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
A8: ( k in dom (upper_volume (chi A,A),(T . i)) & (upper_volume (chi A,A),(T . i)) . k = x1 ) by PARTFUN1:26;
reconsider D = T . i as Division of A ;
A9: 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;
k in Seg (len (upper_volume (chi A,A),(T . i))) by A8, FINSEQ_1:def 3;
then k in Seg (len D) by INTEGRA1:def 7;
then A12: k in dom D by FINSEQ_1:def 3;
then A11: x1 = vol (divset D,k) by A8, INTEGRA1:22;
(sup (divset D,k)) - (inf (divset D,k)) = (vol A) / (i + 1)

proof

A13: now

assume A14: k = 1 ; :: thesis: (sup (divset D,k)) - (inf (divset D,k)) = (vol A) / (i + 1)
then A15: ( inf (divset D,k) = inf A & sup (divset D,k) = D . 1 ) by A12, INTEGRA1:def 5;
( len D = i + 1 & ( for j being Element of NAT st j in dom D holds
D . j = (inf A) + (((vol A) / (len D)) * j) ) ) by A9, INTEGRA4:def 1;
then sup (divset D,k) = (inf A) + (((vol A) / (i + 1)) * 1) by A12, A14, A15;
then (sup (divset D,k)) - (inf (divset D,k)) = ((inf A) + ((vol A) / (i + 1))) - (inf A) by A12, A14, INTEGRA1:def 5;
hence (sup (divset D,k)) - (inf (divset D,k)) = (vol A) / (i + 1) ; :: thesis: verum

end;

now

assume A16: k <> 1 ; :: thesis: (sup (divset D,k)) - (inf (divset D,k)) = (vol A) / (i + 1)
then A17: ( inf (divset D,k) = D . (k - 1) & sup (divset D,k) = D . k ) by A12, INTEGRA1:def 5;
( k - 1 in dom D & k - 1 in NAT ) by A12, A16, INTEGRA1:9;
then ( D . (k - 1) = (inf A) + (((vol A) / (len D)) * (k - 1)) & D . k = (inf A) + (((vol A) / (len D)) * k) ) by A9, A12, INTEGRA4:def 1;
hence (sup (divset D,k)) - (inf (divset D,k)) = (vol A) / (i + 1) by A9, A17, INTEGRA4:def 1; :: thesis: verum

end;

hence (sup (divset D,k)) - (inf (divset D,k)) = (vol A) / (i + 1) by A13; :: thesis: verum

end;

hence x1 in {((vol A) / (i + 1))} by A11, TARSKI:def 1; :: thesis: verum

end;

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

proof

let x1 be set ; :: 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;
reconsider D = T . i as Division of A ;
rng D <> {} ;
then A20: 1 in dom D by FINSEQ_3:34;
then A21: 1 in Seg (len D) by FINSEQ_1:def 3;
B21: 1 in dom D by A20;
1 in Seg (len (upper_volume (chi A,A),D)) by A21, INTEGRA1:def 7;
then 1 in dom (upper_volume (chi A,A),D) by FINSEQ_1:def 3;
then A22: (upper_volume (chi A,A),D) . 1 in rng (upper_volume (chi A,A),D) by FUNCT_1:def 5;
A23: (upper_volume (chi A,A),D) . 1 = vol (divset D,1) by B21, INTEGRA1:22;
A24: ( sup (divset D,1) = D . 1 & inf (divset D,1) = inf A ) by A20, INTEGRA1:def 5;
A25: 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;
then sup (divset D,1) = (inf A) + (((vol A) / (len D)) * 1) by A20, A24, INTEGRA4:def 1;
then vol (divset D,1) = ((inf A) + ((vol A) / (len D))) - (inf A) by A20, INTEGRA1:def 5;
hence x1 in rng (upper_volume (chi A,A),(T . i)) by A19, A22, A23, A25, INTEGRA4:def 1; :: thesis: verum

end;

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

end;

then (delta T) . i in {((vol A) / (i + 1))} by A7, XXREAL_2:def 8;
hence (delta T) . i = (vol A) / (i + 1) by TARSKI:def 1; :: thesis: verum

end;

A26: for i, j being Element of NAT st i <= j holds
(delta T) . i >= (delta T) . j

proof

let i, j be Element of NAT ; :: thesis: ( i <= j implies (delta T) . i >= (delta T) . j )
assume i <= j ; :: thesis: (delta T) . i >= (delta T) . j
then A27: i + 1 <= j + 1 by XREAL_1:8;
vol A >= 0 by INTEGRA1:11;
then (vol A) / (i + 1) >= (vol A) / (j + 1) by A27, XREAL_1:120;
then (delta T) . i >= (vol A) / (j + 1) by A6;
hence (delta T) . i >= (delta T) . j by A6; :: thesis: verum

end;

A28: for a being Real st 0 < a holds
ex i being Element of NAT st abs (((delta T) . i) - 0 ) < a

proof

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

end;

A34: for a being real number st 0 < a holds
ex i being Element of NAT st
for j being Element of NAT st i <= j holds
abs (((delta T) . j) - 0 ) < a

proof

let a be real number ; :: thesis: ( 0 < a implies ex i being Element of NAT st
for j being Element of NAT st i <= j holds
abs (((delta T) . j) - 0 ) < a )
A35: a is Real by XREAL_0:def 1;
assume 0 < a ; :: thesis: ex i being Element of NAT st
for j being Element of NAT st i <= j holds
abs (((delta T) . j) - 0 ) < a
then consider i being Element of NAT such that
A36: abs (((delta T) . i) - 0 ) < a by A28, A35;
(delta T) . i = delta (T . i) by INTEGRA2:def 3;
then (delta T) . i >= 0 by INTEGRA3:8;
then A37: (delta T) . i < a by A36, ABSVALUE:def 1;

now

let j be Element of NAT ; :: thesis: ( i <= j implies abs (((delta T) . j) - 0 ) < a )
assume i <= j ; :: thesis: abs (((delta T) . j) - 0 ) < a
then A38: (delta T) . j <= (delta T) . i by A26;
(delta T) . j = delta (T . j) by INTEGRA2:def 3;
then ( (delta T) . j < a & (delta T) . j >= 0 ) by A37, A38, INTEGRA3:8, XXREAL_0:2;
hence abs (((delta T) . j) - 0 ) < a by ABSVALUE:def 1; :: thesis: verum

end;

hence ex i being Element of NAT st
for j being Element of NAT st i <= j holds
abs (((delta T) . j) - 0 ) < a ; :: thesis: verum

end;

then A39: delta T is convergent by SEQ_2:def 6;
then lim (delta T) = 0 by A34, SEQ_2:def 7;
hence ex T being DivSequence of A st
( delta T is convergent & lim (delta T) = 0 & ( for n being Element of NAT ex Tn being Division of A st
( Tn divide_into_equal n + 1 & T . n = Tn ) ) ) by A5, A39; :: thesis: verum