let a, b be Real; :: thesis: for A being non empty closed_interval Subset of REAL st a < b & A = [.a,b.] holds
for n being Nat st n > 0 holds
ex D being Division of A st D divide_into_equal n

let A be non empty closed_interval Subset of REAL; :: thesis: ( a < b & A = [.a,b.] implies for n being Nat st n > 0 holds
ex D being Division of A st D divide_into_equal n )

assume that
A1: a < b and
A2: A = [.a,b.] ; :: thesis: for n being Nat st n > 0 holds
ex D being Division of A st D divide_into_equal n

A3: b - a > 0 by ;
hereby :: thesis: verum
let n be Nat; :: thesis: ( n > 0 implies ex D being Division of A st D divide_into_equal n )
assume A4: n > 0 ; :: thesis: ex D being Division of A st D divide_into_equal n
defpred S1[ 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 S1[k,r]
proof
let k be Nat; :: thesis: ( k in Seg n implies ex r being Element of REAL st S1[k,r] )
assume k in Seg n ; :: thesis: ex r being Element of REAL st S1[k,r]
a + (((b - a) * k) / n) is Element of REAL by XREAL_0:def 1;
hence ex r being Element of REAL st S1[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
S1[k,D . k] ) ) from reconsider D = D as non empty FinSequence of REAL by A6, A4;
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 ;
k < k + 1 by NAT_1:13;
then (b - a) * k < (b - a) * (k + 1) by ;
then ((b - a) * k) / n < ((b - a) * (k + 1)) / n by ;
hence D . k < D . (k + 1) by ; :: 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 ;
then ( 0 < k / n & k / n <= 1 ) by ;
then ( 0 < (b - a) * (k / n) & (b - a) * (k / n) <= b - a ) by ;
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 ;
hence x in A by ; :: 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 ;
then D . (len D) = a + (((b - a) * n) / n) by ;
then A14: D . (len D) = a + (b - a) by ;
A = [.(),().] by INTEGRA1:4;
then upper_bound A = b by ;
then reconsider D = D as Division of A by ;
for k being Nat st k in dom D holds
D . k = () + (((vol A) / (len D)) * k)
proof
let k be Nat; :: thesis: ( k in dom D implies D . k = () + (((vol A) / (len D)) * k) )
assume k in dom D ; :: thesis: D . k = () + (((vol A) / (len D)) * k)
then A15: D . k = a + (((b - a) * k) / n) by A6;
A = [.(),().] by INTEGRA1:4;
then A16: ( lower_bound A = a & upper_bound A = b ) by ;
then vol A = b - a by INTEGRA1:def 5;
hence D . k = () + (((vol A) / (len D)) * k) by ; :: thesis: verum
end;
hence ex D being Division of A st D divide_into_equal n by ; :: thesis: verum
end;