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
( len D = n & ( for i being Nat st i in dom D holds
D . i = () + (((vol A) / n) * i) ) )

let n be Nat; :: thesis: ( n > 0 & vol A > 0 implies ex D being Division of A st
( len D = n & ( for i being Nat st i in dom D holds
D . i = () + (((vol A) / n) * i) ) ) )

assume that
A1: n > 0 and
A2: vol A > 0 ; :: thesis: ex D being Division of A st
( len D = n & ( for i being Nat st i in dom D holds
D . i = () + (((vol A) / n) * i) ) )

deffunc H1( Nat) -> Element of REAL = In ((() + (((vol A) / n) * \$1)),REAL);
consider D being FinSequence of REAL such that
A3: ( len D = n & ( for i being Nat st i in dom D holds
D . i = H1(i) ) ) from A4: for i, j being Nat st i in dom D & j in dom D & i < j holds
D . i < D . j
proof
let i, j be Nat; :: thesis: ( i in dom D & j in dom D & i < j implies D . i < D . j )
assume that
A5: i in dom D and
A6: j in dom D and
A7: i < j ; :: thesis: D . i < D . j
(vol A) / n > 0 by ;
then ((vol A) / n) * i < ((vol A) / n) * j by ;
then H1(i) < H1(j) by XREAL_1:6;
then D . i < H1(j) by A3, A5;
hence D . i < D . j by A3, A6; :: thesis: verum
end;
A8: dom D = Seg n by ;
reconsider D = D as non empty increasing FinSequence of REAL by ;
D . (len D) = H1(n) by ;
then A9: D . (len D) = () + (vol A) by ;
for x1 being object st x1 in rng D holds
x1 in A
proof
let x1 be object ; :: 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
A10: i in dom D and
A11: D . i = x1 by PARTFUN1:3;
A12: 1 <= i by ;
i <= len D by ;
then ((vol A) / n) * i <= ((vol A) / n) * n by ;
then ((vol A) / n) * i <= vol A by ;
then A13: (lower_bound A) + (((vol A) / n) * i) <= () + (vol A) by XREAL_1:6;
(vol A) / n > 0 by ;
then A14: lower_bound A <= () + (((vol A) / n) * i) by ;
x1 = H1(i) by A3, A10, A11;
hence x1 in A by ; :: thesis: verum
end;
then rng D c= A ;
then reconsider D = D as Division of A by ;
take D ; :: thesis: ( len D = n & ( for i being Nat st i in dom D holds
D . i = () + (((vol A) / n) * i) ) )

thus len D = n by A3; :: thesis: for i being Nat st i in dom D holds
D . i = () + (((vol A) / n) * i)

let i be Nat; :: thesis: ( i in dom D implies D . i = () + (((vol A) / n) * i) )
assume i in dom D ; :: thesis: D . i = () + (((vol A) / n) * i)
then D . i = H1(i) by A3;
hence D . i = () + (((vol A) / n) * i) ; :: thesis: verum