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 = (lower_bound A) + (((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 = (lower_bound A) + (((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 = (lower_bound A) + (((vol A) / n) * i) ) )

deffunc H_{1}( Nat) -> Element of REAL = In (((lower_bound A) + (((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 = H_{1}(i) ) )
from FINSEQ_2:sch 1();

A4: for i, j being Nat st i in dom D & j in dom D & i < j holds

D . i < D . j

reconsider D = D as non empty increasing FinSequence of REAL by A1, A3, A4, SEQM_3:def 1;

D . (len D) = H_{1}(n)
by A3, A8, FINSEQ_1:3;

then A9: D . (len D) = (lower_bound A) + (vol A) by A1, XCMPLX_1:87;

for x1 being object st x1 in rng D holds

x1 in A

then reconsider D = D as Division of A by A9, INTEGRA1:def 2;

take D ; :: thesis: ( len D = n & ( for i being Nat st i in dom D holds

D . i = (lower_bound A) + (((vol A) / n) * i) ) )

thus len D = n by A3; :: thesis: for i being Nat st i in dom D holds

D . i = (lower_bound A) + (((vol A) / n) * i)

let i be Nat; :: thesis: ( i in dom D implies D . i = (lower_bound A) + (((vol A) / n) * i) )

assume i in dom D ; :: thesis: D . i = (lower_bound A) + (((vol A) / n) * i)

then D . i = H_{1}(i)
by A3;

hence D . i = (lower_bound A) + (((vol A) / n) * i) ; :: thesis: verum

ex D being Division of A st

( len D = n & ( for i being Nat st i in dom D holds

D . i = (lower_bound A) + (((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 = (lower_bound A) + (((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 = (lower_bound A) + (((vol A) / n) * i) ) )

deffunc H

consider D being FinSequence of REAL such that

A3: ( len D = n & ( for i being Nat st i in dom D holds

D . i = H

A4: for i, j being Nat st i in dom D & j in dom D & i < j holds

D . i < D . j

proof

A8:
dom D = Seg n
by A3, FINSEQ_1:def 3;
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 A1, A2, XREAL_1:139;

then ((vol A) / n) * i < ((vol A) / n) * j by A7, XREAL_1:68;

then H_{1}(i) < H_{1}(j)
by XREAL_1:6;

then D . i < H_{1}(j)
by A3, A5;

hence D . i < D . j by A3, A6; :: thesis: verum

end;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 A1, A2, XREAL_1:139;

then ((vol A) / n) * i < ((vol A) / n) * j by A7, XREAL_1:68;

then H

then D . i < H

hence D . i < D . j by A3, A6; :: thesis: verum

reconsider D = D as non empty increasing FinSequence of REAL by A1, A3, A4, SEQM_3:def 1;

D . (len D) = H

then A9: D . (len D) = (lower_bound A) + (vol A) by A1, XCMPLX_1:87;

for x1 being object st x1 in rng D holds

x1 in A

proof

then
rng D c= A
;
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 A10, FINSEQ_3:25;

i <= len D by A10, FINSEQ_3:25;

then ((vol A) / n) * i <= ((vol A) / n) * n by A2, A3, XREAL_1:64;

then ((vol A) / n) * i <= vol A by A1, XCMPLX_1:87;

then A13: (lower_bound A) + (((vol A) / n) * i) <= (lower_bound A) + (vol A) by XREAL_1:6;

(vol A) / n > 0 by A1, A2, XREAL_1:139;

then A14: lower_bound A <= (lower_bound A) + (((vol A) / n) * i) by A12, XREAL_1:29, XREAL_1:129;

x1 = H_{1}(i)
by A3, A10, A11;

hence x1 in A by A14, A13, INTEGRA2:1; :: thesis: verum

end;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 A10, FINSEQ_3:25;

i <= len D by A10, FINSEQ_3:25;

then ((vol A) / n) * i <= ((vol A) / n) * n by A2, A3, XREAL_1:64;

then ((vol A) / n) * i <= vol A by A1, XCMPLX_1:87;

then A13: (lower_bound A) + (((vol A) / n) * i) <= (lower_bound A) + (vol A) by XREAL_1:6;

(vol A) / n > 0 by A1, A2, XREAL_1:139;

then A14: lower_bound A <= (lower_bound A) + (((vol A) / n) * i) by A12, XREAL_1:29, XREAL_1:129;

x1 = H

hence x1 in A by A14, A13, INTEGRA2:1; :: thesis: verum

then reconsider D = D as Division of A by A9, INTEGRA1:def 2;

take D ; :: thesis: ( len D = n & ( for i being Nat st i in dom D holds

D . i = (lower_bound A) + (((vol A) / n) * i) ) )

thus len D = n by A3; :: thesis: for i being Nat st i in dom D holds

D . i = (lower_bound A) + (((vol A) / n) * i)

let i be Nat; :: thesis: ( i in dom D implies D . i = (lower_bound A) + (((vol A) / n) * i) )

assume i in dom D ; :: thesis: D . i = (lower_bound A) + (((vol A) / n) * i)

then D . i = H

hence D . i = (lower_bound A) + (((vol A) / n) * i) ; :: thesis: verum