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 & ( for n being Element of NAT ex Tn being Division of A st

( Tn divide_into_equal n + 1 & T . n = Tn ) ) ) )

defpred S_{1}[ 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 (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 ) ) )

A2: for n being Element of NAT ex D being Element of divs A st S_{1}[n,D]

A4: for n being Element of NAT holds S_{1}[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 )

ex i being Element of NAT st |.(((delta T) . i) - 0).| < a

(delta T) . i >= (delta T) . j

ex i being Nat st

for j being Nat st i <= j holds

|.(((delta T) . j) - 0).| < a

then lim (delta T) = 0 by A31, 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, A36; :: thesis: verum

( 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

( 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 & ( 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 S

proof

consider T being sequence of (divs A) such that
let n be Element of NAT ; :: thesis: ex D being Element of divs A st S_{1}[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 = (lower_bound 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_{1}[n,D1]

D divide_into_equal n + 1 by A3, INTEGRA4:def 1;

hence S_{1}[n,D1]
; :: thesis: verum

end;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 = (lower_bound 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

D divide_into_equal n + 1 by A3, INTEGRA4:def 1;

hence S

A4: for n being Element of NAT holds S

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

A6:
for i being Element of NAT holds (delta T) . i = (vol A) / (i + 1)
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;( 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

proof

A24:
for a being Real st 0 < a holds
let i be Element of NAT ; :: thesis: (delta T) . 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))}

for x1 being object st x1 in {((vol A) / (i + 1))} holds

x1 in 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 A18, INTEGRA3:def 2, XBOOLE_0:def 10;

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;for x1 being object st x1 in rng (upper_volume ((chi (A,A)),(T . i))) holds

x1 in {((vol A) / (i + 1))}

proof

then A18:
rng (upper_volume ((chi (A,A)),(T . i))) c= {((vol A) / (i + 1))}
;
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 A7, FINSEQ_1:def 3;

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)

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

end;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 A7, FINSEQ_1:def 3;

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

end;

x1 = vol (divset (D,k))
by A8, A9, INTEGRA1:20;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 A10, INTEGRA4:def 1;

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 A9, INTEGRA1:def 4;

then upper_bound (divset (D,k)) = (lower_bound A) + (((vol A) / (i + 1)) * 1) by A10, A9, A14, A13, INTEGRA4:def 1;

then (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) = ((lower_bound A) + ((vol A) / (i + 1))) - (lower_bound A) by A9, A14, INTEGRA1:def 4;

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

end;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 A9, INTEGRA1:def 4;

then upper_bound (divset (D,k)) = (lower_bound A) + (((vol A) / (i + 1)) * 1) by A10, A9, A14, A13, INTEGRA4:def 1;

then (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) = ((lower_bound A) + ((vol A) / (i + 1))) - (lower_bound A) by A9, A14, INTEGRA1:def 4;

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

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

hence
(upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) = (vol A) / (i + 1)
by A12; :: thesis: verumassume 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 A9, INTEGRA1:7;

then A16: D . (k - 1) = (lower_bound A) + (((vol A) / (len D)) * (k - 1)) by A10, INTEGRA4:def 1;

A17: D . k = (lower_bound A) + (((vol A) / (len D)) * k) by A10, A9, INTEGRA4:def 1;

( lower_bound (divset (D,k)) = D . (k - 1) & upper_bound (divset (D,k)) = D . k ) by A9, A15, INTEGRA1:def 4;

hence (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) = (vol A) / (i + 1) by A10, A16, A17, INTEGRA4:def 1; :: thesis: verum

end;then k - 1 in dom D by A9, INTEGRA1:7;

then A16: D . (k - 1) = (lower_bound A) + (((vol A) / (len D)) * (k - 1)) by A10, INTEGRA4:def 1;

A17: D . k = (lower_bound A) + (((vol A) / (len D)) * k) by A10, A9, INTEGRA4:def 1;

( lower_bound (divset (D,k)) = D . (k - 1) & upper_bound (divset (D,k)) = D . k ) by A9, A15, INTEGRA1:def 4;

hence (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) = (vol A) / (i + 1) by A10, A16, A17, INTEGRA4:def 1; :: thesis: verum

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

for x1 being object st x1 in {((vol A) / (i + 1))} holds

x1 in rng (upper_volume ((chi (A,A)),(T . i)))

proof

then
{((vol A) / (i + 1))} c= rng (upper_volume ((chi (A,A)),(T . i)))
;
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)) = (lower_bound A) + (((vol A) / (len D)) * 1) by A21, A20, INTEGRA4:def 1;

then A22: vol (divset (D,1)) = ((lower_bound A) + ((vol A) / (len D))) - (lower_bound A) by A21, INTEGRA1:def 4;

1 in Seg (len D) by A21, 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 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 A21, INTEGRA1:20;

hence x1 in rng (upper_volume ((chi (A,A)),(T . i))) by A19, A23, A20, A22, INTEGRA4:def 1; :: thesis: verum

end;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)) = (lower_bound A) + (((vol A) / (len D)) * 1) by A21, A20, INTEGRA4:def 1;

then A22: vol (divset (D,1)) = ((lower_bound A) + ((vol A) / (len D))) - (lower_bound A) by A21, INTEGRA1:def 4;

1 in Seg (len D) by A21, 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 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 A21, INTEGRA1:20;

hence x1 in rng (upper_volume ((chi (A,A)),(T . i))) by A19, A23, A20, A22, INTEGRA4:def 1; :: thesis: verum

then ( (delta T) . i = delta (T . i) & rng (upper_volume ((chi (A,A)),(T . i))) = {((vol A) / (i + 1))} ) by A18, INTEGRA3:def 2, XBOOLE_0:def 10;

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

ex i being Element of NAT st |.(((delta T) . i) - 0).| < a

proof

A29:
for i, j being Element of NAT st i <= j holds
let a be Real; :: thesis: ( 0 < a implies ex i being Element of NAT st |.(((delta T) . 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 |.(((delta T) . i) - 0).| < a

then [\((vol A) / a)/] + 1 > 0 by A25, 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 A27: (vol A) / (i1 + 1) < 1 * a by A26, XREAL_1:113;

A28: (delta T) . i1 = (vol A) / (i1 + 1) by A6;

((vol A) / (i1 + 1)) - 0 = |.(((vol A) / (i1 + 1)) - 0).| by A25, ABSVALUE:def 1;

hence ex i being Element of NAT st |.(((delta T) . i) - 0).| < a by A27, A28; :: thesis: verum

end;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 |.(((delta T) . i) - 0).| < a

then [\((vol A) / a)/] + 1 > 0 by A25, 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 A27: (vol A) / (i1 + 1) < 1 * a by A26, XREAL_1:113;

A28: (delta T) . i1 = (vol A) / (i1 + 1) by A6;

((vol A) / (i1 + 1)) - 0 = |.(((vol A) / (i1 + 1)) - 0).| by A25, ABSVALUE:def 1;

hence ex i being Element of NAT st |.(((delta T) . i) - 0).| < a by A27, A28; :: thesis: verum

(delta T) . i >= (delta T) . j

proof

A31:
for a being Real st 0 < a holds
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 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 A30, XREAL_1:118;

then (delta T) . i >= (vol A) / (j + 1) by A6;

hence (delta T) . i >= (delta T) . j by A6; :: thesis: verum

end;assume i <= j ; :: thesis: (delta T) . i >= (delta T) . 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 A30, XREAL_1:118;

then (delta T) . i >= (vol A) / (j + 1) by A6;

hence (delta T) . i >= (delta T) . j by A6; :: thesis: verum

ex i being Nat st

for j being Nat st i <= j holds

|.(((delta T) . j) - 0).| < a

proof

then A36:
delta T is convergent
by SEQ_2:def 6;
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 A32: 0 < a ; :: thesis: ex i being Nat st

for j being Nat st i <= j holds

|.(((delta T) . j) - 0).| < a

consider i being Element of NAT such that

A33: |.(((delta T) . i) - 0).| < a by A24, A32;

(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 A33, ABSVALUE:def 1;

take i ; :: thesis: for j being Nat st i <= j holds

|.(((delta T) . j) - 0).| < a

let j be Nat; :: thesis: ( i <= j implies |.(((delta T) . j) - 0).| < a )

reconsider jj = j as Element of NAT by ORDINAL1:def 12;

assume i <= j ; :: thesis: |.(((delta T) . j) - 0).| < a

then (delta T) . jj <= (delta T) . i by A29;

then A35: (delta T) . j < a by A34, XXREAL_0:2;

(delta T) . j = delta (T . jj) by INTEGRA3:def 2;

then (delta T) . j >= 0 by INTEGRA3:9;

hence |.(((delta T) . j) - 0).| < a by A35, ABSVALUE:def 1; :: thesis: verum

end;for j being Nat st i <= j holds

|.(((delta T) . j) - 0).| < a )

assume A32: 0 < a ; :: thesis: ex i being Nat st

for j being Nat st i <= j holds

|.(((delta T) . j) - 0).| < a

consider i being Element of NAT such that

A33: |.(((delta T) . i) - 0).| < a by A24, A32;

(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 A33, ABSVALUE:def 1;

take i ; :: thesis: for j being Nat st i <= j holds

|.(((delta T) . j) - 0).| < a

let j be Nat; :: thesis: ( i <= j implies |.(((delta T) . j) - 0).| < a )

reconsider jj = j as Element of NAT by ORDINAL1:def 12;

assume i <= j ; :: thesis: |.(((delta T) . j) - 0).| < a

then (delta T) . jj <= (delta T) . i by A29;

then A35: (delta T) . j < a by A34, XXREAL_0:2;

(delta T) . j = delta (T . jj) by INTEGRA3:def 2;

then (delta T) . j >= 0 by INTEGRA3:9;

hence |.(((delta T) . j) - 0).| < a by A35, ABSVALUE:def 1; :: thesis: verum

then lim (delta T) = 0 by A31, 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, A36; :: thesis: verum