let A be non empty closed_interval Subset of REAL; :: thesis: for D being Division of A st 0 < vol A & D . 1 = lower_bound A holds
D /^ 1 is Division of A
let D be Division of A; :: thesis: ( 0 < vol A & D . 1 = lower_bound A implies D /^ 1 is Division of A )
assume A1: ( 0 < vol A & D . 1 = lower_bound A ) ; :: thesis: D /^ 1 is Division of A
0 < len D ;
then A2: 0 + 1 <= len D by NAT_1:13;
1 <> len D

proof

assume 1 = len D ; :: thesis: contradiction
then D . 1 = upper_bound A by INTEGRA1:def 2;
hence contradiction by A1; :: thesis: verum

end;

then 1 < len D by A2, XXREAL_0:1;
then 1 + 1 <= len D by NAT_1:13;
then A5: (1 + 1) - 1 <= (len D) - 1 by XREAL_1:9;
A6: (len D) - 1 = len (D /^ 1) by A2, RFINSEQ:def 1;
A8: len (D /^ 1) <> 0 by A5, RFINSEQ:def 1, A2;
then len (D /^ 1) in Seg (len (D /^ 1)) by FINSEQ_1:3;
then A9: len (D /^ 1) in dom (D /^ 1) by FINSEQ_1:def 3;
for e1, e2 being Nat st e1 in dom (D /^ 1) & e2 in dom (D /^ 1) & e1 < e2 holds
(D /^ 1) . e1 < (D /^ 1) . e2

proof

let e1, e2 be Nat; :: thesis: ( e1 in dom (D /^ 1) & e2 in dom (D /^ 1) & e1 < e2 implies (D /^ 1) . e1 < (D /^ 1) . e2 )
assume A10: ( e1 in dom (D /^ 1) & e2 in dom (D /^ 1) & e1 < e2 ) ; :: thesis: (D /^ 1) . e1 < (D /^ 1) . e2
then A11: ( (D /^ 1) . e1 = D . (e1 + 1) & (D /^ 1) . e2 = D . (e2 + 1) ) by A2, RFINSEQ:def 1;
( 1 <= e1 & e1 <= len (D /^ 1) ) by A10, FINSEQ_3:25;
then ( 1 + 0 <= e1 + 1 & e1 + 1 <= (len (D /^ 1)) + 1 ) by XREAL_1:7;
then A14: e1 + 1 in dom D by A6, FINSEQ_3:25;
( 1 <= e2 & e2 <= len (D /^ 1) ) by A10, FINSEQ_3:25;
then ( 1 + 0 <= e2 + 1 & e2 + 1 <= (len (D /^ 1)) + 1 ) by XREAL_1:7;
then A15: e2 + 1 in dom D by FINSEQ_3:25, A6;
e1 + 1 < e2 + 1 by A10, XREAL_1:8;
hence (D /^ 1) . e1 < (D /^ 1) . e2 by A11, A14, A15, VALUED_0:def 13; :: thesis: verum

end;

then A16: D /^ 1 is increasing ;
A17: len (D /^ 1) = (len D) - 1 by A2, RFINSEQ:def 1;
B23: for x being object st x in rng (D /^ 1) holds
x in rng D

proof

let x be object ; :: thesis: ( x in rng (D /^ 1) implies x in rng D )
assume x in rng (D /^ 1) ; :: thesis: x in rng D
then consider m being Nat such that
A18: m in dom (D /^ 1) and
A19: (D /^ 1) . m = x by FINSEQ_2:10;
B20: m <= len (D /^ 1) by A18, FINSEQ_3:25;
1 <= m + 1 by NAT_1:11;
then A22: m + 1 in dom D by B20, A17, XREAL_1:19, FINSEQ_3:25;
(D /^ 1) . m = D . (m + 1) by A2, A18, RFINSEQ:def 1;
hence x in rng D by A19, A22, FUNCT_1:def 3; :: thesis: verum

end;

rng D c= A by INTEGRA1:def 2;
then A24: rng (D /^ 1) c= A by B23;
A25: (D /^ 1) . (len (D /^ 1)) = D . ((len (D /^ 1)) + 1) by A2, A9, RFINSEQ:def 1
.= D . (((len D) - 1) + 1) by A2, RFINSEQ:def 1
.= upper_bound A by INTEGRA1:def 2 ;
D /^ 1 <> {} by A8;
hence D /^ 1 is Division of A by A16, A24, A25, INTEGRA1:def 2; :: thesis: verum