let A be non empty closed_interval Subset of REAL; :: thesis: for D2 being Division of A st lower_bound A < D2 . 1 holds
<*(lower_bound A)*> ^ D2 is non empty increasing FinSequence of REAL
let D2 be Division of A; :: thesis: ( lower_bound A < D2 . 1 implies <*(lower_bound A)*> ^ D2 is non empty increasing FinSequence of REAL )
set MD2 = <*(lower_bound A)*> ^ D2;
assume A1: lower_bound A < D2 . 1 ; :: thesis: <*(lower_bound A)*> ^ D2 is non empty increasing FinSequence of REAL
for n, m being Element of NAT st n in dom (<*(lower_bound A)*> ^ D2) & m in dom (<*(lower_bound A)*> ^ D2) & n < m holds
(<*(lower_bound A)*> ^ D2) . n < (<*(lower_bound A)*> ^ D2) . m

proof

let n, m be Element of NAT ; :: thesis: ( n in dom (<*(lower_bound A)*> ^ D2) & m in dom (<*(lower_bound A)*> ^ D2) & n < m implies (<*(lower_bound A)*> ^ D2) . n < (<*(lower_bound A)*> ^ D2) . m )
assume that
A2: n in dom (<*(lower_bound A)*> ^ D2) and
A3: m in dom (<*(lower_bound A)*> ^ D2) and
A4: n < m ; :: thesis: (<*(lower_bound A)*> ^ D2) . n < (<*(lower_bound A)*> ^ D2) . m
A5: not m in dom <*(lower_bound A)*>

proof

assume m in dom <*(lower_bound A)*> ; :: thesis: contradiction
then m in Seg (len <*(lower_bound A)*>) by FINSEQ_1:def 3;
then m in {1} by FINSEQ_1:2, FINSEQ_1:39;
then A6: n < 1 by A4, TARSKI:def 1;
n in Seg (len (<*(lower_bound A)*> ^ D2)) by A2, FINSEQ_1:def 3;
hence contradiction by A6, FINSEQ_1:1; :: thesis: verum

end;

A7: not (<*(lower_bound A)*> ^ D2) . m in rng <*(lower_bound A)*>

proof

assume (<*(lower_bound A)*> ^ D2) . m in rng <*(lower_bound A)*> ; :: thesis: contradiction
then (<*(lower_bound A)*> ^ D2) . m in {(lower_bound A)} by FINSEQ_1:38;
then A8: (<*(lower_bound A)*> ^ D2) . m = lower_bound A by TARSKI:def 1;
rng D2 <> {} ;
then A9: 1 in dom D2 by FINSEQ_3:32;
consider n being Nat such that
A10: n in dom D2 and
A11: m = (len <*(lower_bound A)*>) + n by A3, A5, FINSEQ_1:25;
n in Seg (len D2) by A10, FINSEQ_1:def 3;
then A12: 1 <= n by FINSEQ_1:1;
D2 . n = (<*(lower_bound A)*> ^ D2) . m by A10, A11, FINSEQ_1:def 7;
hence contradiction by A1, A8, A10, A12, A9, SEQ_4:137; :: thesis: verum

end;

(<*(lower_bound A)*> ^ D2) . m in rng (<*(lower_bound A)*> ^ D2) by A3, FUNCT_1:def 3;
then (<*(lower_bound A)*> ^ D2) . m in (rng <*(lower_bound A)*>) \/ (rng D2) by FINSEQ_1:31;
then A13: ( (<*(lower_bound A)*> ^ D2) . m in rng <*(lower_bound A)*> or (<*(lower_bound A)*> ^ D2) . m in rng D2 ) by XBOOLE_0:def 3;

now

per cases ( n in dom <*(lower_bound A)*> or ex i being Nat st
( i in dom D2 & n = (len <*(lower_bound A)*>) + i ) ) by A2, FINSEQ_1:25;

suppose A14: n in dom <*(lower_bound A)*> ; :: thesis: (<*(lower_bound A)*> ^ D2) . n < (<*(lower_bound A)*> ^ D2) . m

then n in Seg (len <*(lower_bound A)*>) by FINSEQ_1:def 3;
then n in {1} by FINSEQ_1:2, FINSEQ_1:39;
then A15: n = 1 by TARSKI:def 1;
A16: (<*(lower_bound A)*> ^ D2) . n = <*(lower_bound A)*> . n by A14, FINSEQ_1:def 7
.= lower_bound A by A15, FINSEQ_1:def 8 ;
rng D2 <> {} ;
then A17: 1 in dom D2 by FINSEQ_3:32;
consider k being Element of NAT such that
A18: k in dom D2 and
A19: (<*(lower_bound A)*> ^ D2) . m = D2 . k by A13, A7, PARTFUN1:3;
k in Seg (len D2) by A18, FINSEQ_1:def 3;
then 1 <= k by FINSEQ_1:1;
then D2 . 1 <= (<*(lower_bound A)*> ^ D2) . m by A18, A19, A17, SEQ_4:137;
hence (<*(lower_bound A)*> ^ D2) . n < (<*(lower_bound A)*> ^ D2) . m by A1, A16, XXREAL_0:2; :: thesis: verum

end;

suppose ex i being Nat st
( i in dom D2 & n = (len <*(lower_bound A)*>) + i ) ; :: thesis: (<*(lower_bound A)*> ^ D2) . n < (<*(lower_bound A)*> ^ D2) . m

then consider i being Element of NAT such that
A20: i in dom D2 and
A21: n = (len <*(lower_bound A)*>) + i ;
A22: D2 . i = (<*(lower_bound A)*> ^ D2) . n by A20, A21, FINSEQ_1:def 7;
consider j being Nat such that
A23: j in dom D2 and
A24: m = (len <*(lower_bound A)*>) + j by A3, A5, FINSEQ_1:25;
A25: D2 . j = (<*(lower_bound A)*> ^ D2) . m by A23, A24, FINSEQ_1:def 7;
i < j by A4, A21, A24, XREAL_1:6;
hence (<*(lower_bound A)*> ^ D2) . n < (<*(lower_bound A)*> ^ D2) . m by A20, A23, A22, A25, SEQM_3:def 1; :: thesis: verum

end;

end;

end;

hence (<*(lower_bound A)*> ^ D2) . n < (<*(lower_bound A)*> ^ D2) . m ; :: thesis: verum

end;

hence <*(lower_bound A)*> ^ D2 is non empty increasing FinSequence of REAL by SEQM_3:def 1; :: thesis: verum