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_{1}[ 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_{1}[k,r]

A6: ( dom D = Seg n & ( for k being Nat st k in Seg n holds

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

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)

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

A5: for k being Nat st k in Seg n holds

ex r being Element of REAL st S

proof

consider D being FinSequence of REAL such that
let k be Nat; :: thesis: ( k in Seg n implies ex r being Element of REAL st S_{1}[k,r] )

assume k in Seg n ; :: thesis: ex r being Element of REAL st S_{1}[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_{1}[k,r]
; :: thesis: verum

end;assume k in Seg n ; :: thesis: ex r being Element of REAL st S

a + (((b - a) * k) / n) is Element of REAL by XREAL_0:def 1;

hence ex r being Element of REAL st S

A6: ( dom D = Seg n & ( for k being Nat st k in Seg n holds

S

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

then reconsider D = D as non empty increasing FinSequence of REAL by EUCLID_7:def 1;
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;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

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

x in A

then A12:
rng D c= A
;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;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

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

hence
ex D being Division of A st D divide_into_equal n
by A13, INTEGRA4:def 1; :: thesis: verum
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;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