let A be non empty closed_interval Subset of REAL; :: thesis: for n being Nat st n > 0 & vol A > 0 holds
ex D being Division of A st D divide_into_equal n
let n be Nat; :: thesis: ( n > 0 & vol A > 0 implies ex D being Division of A st D divide_into_equal n )
assume A1: n > 0 ; :: thesis: ( not vol A > 0 or ex D being Division of A st D divide_into_equal n )
assume A2: vol A > 0 ; :: thesis: ex D being Division of A st D divide_into_equal n
consider a, b being Real such that
a <= b and
A3: A = [.a,b.] by MEASURE5:14;
A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;
then ( lower_bound A = a & upper_bound A = b ) by A3, INTEGRA1:5;
then A4: b - a > 0 by A2, INTEGRA1:def 5;
defpred S₁[ Nat, Real] means $2 = a + (((b - a) * $1) / n);
A5: for k being Nat st k in Seg n holds
ex r being Element of REAL st S₁[k,r]

proof

let k be Nat; :: thesis: ( k in Seg n implies ex r being Element of REAL st S₁[k,r] )
assume k in Seg n ; :: thesis: ex r being Element of REAL st S₁[k,r]
a + (((b - a) * k) / n) is Element of REAL by XREAL_0:def 1;
hence ex r being Element of REAL st S₁[k,r] ; :: thesis: verum

end;

consider D being FinSequence of REAL such that
A6: ( dom D = Seg n & ( for k being Nat st k in Seg n holds
S₁[k,D . k] ) ) from FINSEQ_1:sch 5(A5);
reconsider D = D as non empty FinSequence of REAL by A6, A1;
for k being Nat st 1 <= k & k < len D holds
D . k < D . (k + 1)

proof

let k be Nat; :: thesis: ( 1 <= k & k < len D implies D . k < D . (k + 1) )
assume A7: ( 1 <= k & k < len D ) ; :: thesis: D . k < D . (k + 1)
then ( 1 <= k + 1 & k + 1 <= len D ) by NAT_1:13;
then A8: ( D . k = a + (((b - a) * k) / n) & D . (k + 1) = a + (((b - a) * (k + 1)) / n) ) by A6, A7, FINSEQ_3:25;
k < k + 1 by NAT_1:13;
then (b - a) * k < (b - a) * (k + 1) by A4, XREAL_1:68;
then ((b - a) * k) / n < ((b - a) * (k + 1)) / n by A1, XREAL_1:74;
hence D . k < D . (k + 1) by A8, XREAL_1:8; :: thesis: verum

end;

then reconsider D = D as non empty increasing FinSequence of REAL by EUCLID_7:def 1;

now :: thesis: for x being object st x in rng D holds
x in A

let x be object ; :: thesis: ( x in rng D implies x in A )
assume x in rng D ; :: thesis: x in A
then consider k being Element of NAT such that
A9: ( k in dom D & x = D . k ) by PARTFUN1:3;
A10: D . k = a + (((b - a) * k) / n) by A6, A9;
( 1 <= k & k <= n ) by A6, A9, FINSEQ_1:1;
then ( 0 < k / n & k / n <= 1 ) by XREAL_1:139, XREAL_1:183;
then ( 0 < (b - a) * (k / n) & (b - a) * (k / n) <= b - a ) by A4, XREAL_1:129, XREAL_1:153;
then A11: ( 0 < ((b - a) * k) / n & ((b - a) * k) / n <= b - a ) by XCMPLX_1:74;
a + (b - a) = b ;
then ( a < a + (((b - a) * k) / n) & a + (((b - a) * k) / n) <= b ) by A11, XREAL_1:29, XREAL_1:6;
hence x in A by A3, A9, A10, XXREAL_1:1; :: thesis: verum

end;

then A12: rng D c= A ;
dom D = Seg (len D) by FINSEQ_1:def 3;
then A13: len D = n by A6, FINSEQ_1:6;
then D . (len D) = a + (((b - a) * n) / n) by A6, FINSEQ_1:3;
then A14: D . (len D) = a + (b - a) by A1, XCMPLX_1:89;
A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;
then upper_bound A = b by A3, INTEGRA1:5;
then reconsider D = D as Division of A by A12, A14, INTEGRA1:def 2;
for k being Nat st k in dom D holds
D . k = (lower_bound A) + (((vol A) / (len D)) * k)

proof

let k be Nat; :: thesis: ( k in dom D implies D . k = (lower_bound A) + (((vol A) / (len D)) * k) )
assume k in dom D ; :: thesis: D . k = (lower_bound A) + (((vol A) / (len D)) * k)
then A15: D . k = a + (((b - a) * k) / n) by A6;
A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;
then A16: ( lower_bound A = a & upper_bound A = b ) by A3, INTEGRA1:5;
then vol A = b - a by INTEGRA1:def 5;
hence D . k = (lower_bound A) + (((vol A) / (len D)) * k) by A13, A15, A16, XCMPLX_1:74; :: thesis: verum

end;

hence ex D being Division of A st D divide_into_equal n by A13, INTEGRA4:def 1; :: thesis: verum