let A be closed-interval Subset of REAL ; :: thesis: for n being Element of NAT st n > 0 & vol A > 0 holds
ex D being Division of A st
( len D = n & ( for i being Element of NAT st i in dom D holds
D . i = (inf A) + (((vol A) / n) * i) ) )
let n be Element of NAT ; :: thesis: ( n > 0 & vol A > 0 implies ex D being Division of A st
( len D = n & ( for i being Element of NAT st i in dom D holds
D . i = (inf A) + (((vol A) / n) * i) ) ) )
assume A1: ( n > 0 & vol A > 0 ) ; :: thesis: ex D being Division of A st
( len D = n & ( for i being Element of NAT st i in dom D holds
D . i = (inf A) + (((vol A) / n) * i) ) )
deffunc H₁( Nat) -> Element of REAL = (inf A) + (((vol A) / n) * $1);
consider D being FinSequence of REAL such that
A2: ( len D = n & ( for i being Nat st i in dom D holds
D . i = H₁(i) ) ) from FINSEQ_2:sch 1();
A3: dom D = Seg n by A2, FINSEQ_1:def 3;
for i, j being Element of NAT st i in dom D & j in dom D & i < j holds
D . i < D . j

proof

let i, j be Element of NAT ; :: thesis: ( i in dom D & j in dom D & i < j implies D . i < D . j )
assume A4: ( i in dom D & j in dom D & i < j ) ; :: thesis: D . i < D . j
(vol A) / n > 0 by A1, XREAL_1:141;
then ((vol A) / n) * i < ((vol A) / n) * j by A4, XREAL_1:70;
then (inf A) + (((vol A) / n) * i) < (inf A) + (((vol A) / n) * j) by XREAL_1:8;
then D . i < (inf A) + (((vol A) / n) * j) by A2, A4;
hence D . i < D . j by A2, A4; :: thesis: verum

end;

then reconsider D = D as non empty increasing FinSequence of REAL by A1, A2, SEQM_3:def 1;
for x1 being set st x1 in rng D holds
x1 in A

proof

let x1 be set ; :: thesis: ( x1 in rng D implies x1 in A )
assume x1 in rng D ; :: thesis: x1 in A
then consider i being Element of NAT such that
A6: ( i in dom D & D . i = x1 ) by PARTFUN1:26;
A7: x1 = (inf A) + (((vol A) / n) * i) by A2, A6;
A8: ( 1 <= i & i <= len D & (vol A) / n > 0 ) by A1, A6, FINSEQ_3:27, XREAL_1:141;
then A9: ((vol A) / n) * i > 0 by XREAL_1:131;
((vol A) / n) * i <= ((vol A) / n) * n by A2, A8, XREAL_1:66;
then ((vol A) / n) * i <= vol A by A1, XCMPLX_1:88;
then ( inf A <= (inf A) + (((vol A) / n) * i) & (inf A) + (((vol A) / n) * i) <= (inf A) + (vol A) ) by A9, XREAL_1:8, XREAL_1:31;
hence x1 in A by A7, INTEGRA2:1; :: thesis: verum

end;

then A10: rng D c= A by TARSKI:def 3;
D . (len D) = (inf A) + (((vol A) / n) * n) by A2, A3, FINSEQ_1:5;
then D . (len D) = (inf A) + (vol A) by A1, XCMPLX_1:88;
then D is Division of A by A10, INTEGRA1:def 2;
then reconsider D = D as Division of A by INTEGRA1:def 3;
take D ; :: thesis: ( len D = n & ( for i being Element of NAT st i in dom D holds
D . i = (inf A) + (((vol A) / n) * i) ) )
thus ( len D = n & ( for i being Element of NAT st i in dom D holds
D . i = (inf A) + (((vol A) / n) * i) ) ) by A2; :: thesis: verum