let A be closed-interval Subset of REAL ; :: thesis: for D1 being Division of A st vol A <> 0 & len D1 = 1 holds
<*(lower_bound A)*> ^ D1 is non empty increasing FinSequence of REAL
let D1 be Division of A; :: thesis: ( vol A <> 0 & len D1 = 1 implies <*(lower_bound A)*> ^ D1 is non empty increasing FinSequence of REAL )
assume A1: vol A <> 0 ; :: thesis: ( not len D1 = 1 or <*(lower_bound A)*> ^ D1 is non empty increasing FinSequence of REAL )
assume len D1 = 1 ; :: thesis: <*(lower_bound A)*> ^ D1 is non empty increasing FinSequence of REAL
then A2: D1 . 1 = upper_bound A by INTEGRA1:def 2;
vol A >= 0 by INTEGRA1:11;
then (D1 . 1) - (lower_bound A) > 0 by A1, A2, INTEGRA1:def 6;
then A3: lower_bound A < D1 . 1 by XREAL_1:49;
set MD1 = <*(lower_bound A)*> ^ D1;
for n, m being Element of NAT st n in dom (<*(lower_bound A)*> ^ D1) & m in dom (<*(lower_bound A)*> ^ D1) & n < m holds
(<*(lower_bound A)*> ^ D1) . n < (<*(lower_bound A)*> ^ D1) . m

proof

let n, m be Element of NAT ; :: thesis: ( n in dom (<*(lower_bound A)*> ^ D1) & m in dom (<*(lower_bound A)*> ^ D1) & n < m implies (<*(lower_bound A)*> ^ D1) . n < (<*(lower_bound A)*> ^ D1) . m )
assume A4: ( n in dom (<*(lower_bound A)*> ^ D1) & m in dom (<*(lower_bound A)*> ^ D1) & n < m ) ; :: thesis: (<*(lower_bound A)*> ^ D1) . n < (<*(lower_bound A)*> ^ D1) . 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:4, FINSEQ_1:56;
then A6: n < 1 by A4, TARSKI:def 1;
n in Seg (len (<*(lower_bound A)*> ^ D1)) by A4, FINSEQ_1:def 3;
hence contradiction by A6, FINSEQ_1:3; :: thesis: verum

end;

(<*(lower_bound A)*> ^ D1) . m in rng (<*(lower_bound A)*> ^ D1) by A4, FUNCT_1:def 5;
then A7: (<*(lower_bound A)*> ^ D1) . m in (rng <*(lower_bound A)*>) \/ (rng D1) by FINSEQ_1:44;
not (<*(lower_bound A)*> ^ D1) . m in rng <*(lower_bound A)*>

proof

assume (<*(lower_bound A)*> ^ D1) . m in rng <*(lower_bound A)*> ; :: thesis: contradiction
then (<*(lower_bound A)*> ^ D1) . m in {(lower_bound A)} by FINSEQ_1:55;
then A8: (<*(lower_bound A)*> ^ D1) . m = lower_bound A by TARSKI:def 1;
consider n being Nat such that
A9: ( n in dom D1 & m = (len <*(lower_bound A)*>) + n ) by A4, A5, FINSEQ_1:38;
n in Seg (len D1) by A9, FINSEQ_1:def 3;
then A10: ( 1 <= n & n <= len D1 ) by FINSEQ_1:3;
rng D1 <> {} ;
then A11: 1 in dom D1 by FINSEQ_3:34;
D1 . n = (<*(lower_bound A)*> ^ D1) . m by A9, FINSEQ_1:def 7;
hence contradiction by A3, A8, A9, A10, A11, GOBOARD2:18; :: thesis: verum

end;

then A12: (<*(lower_bound A)*> ^ D1) . m in rng D1 by A7, XBOOLE_0:def 3;

now

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

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

then n in Seg (len <*(lower_bound A)*>) by FINSEQ_1:def 3;
then n in {1} by FINSEQ_1:4, FINSEQ_1:56;
then A14: n = 1 by TARSKI:def 1;
consider k being Element of NAT such that
A15: ( k in dom D1 & (<*(lower_bound A)*> ^ D1) . m = D1 . k ) by A12, PARTFUN1:26;
A16: ( 1 <= k & k <= len D1 ) by A15, FINSEQ_3:27;
rng D1 <> {} ;
then 1 in dom D1 by FINSEQ_3:34;
then A17: D1 . 1 <= (<*(lower_bound A)*> ^ D1) . m by A15, A16, GOBOARD2:18;
(<*(lower_bound A)*> ^ D1) . n = <*(lower_bound A)*> . n by A13, FINSEQ_1:def 7
.= lower_bound A by A14, FINSEQ_1:def 8 ;
hence (<*(lower_bound A)*> ^ D1) . n < (<*(lower_bound A)*> ^ D1) . m by A3, A17, XXREAL_0:2; :: thesis: verum

end;

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

then consider i being Element of NAT such that
A18: ( i in dom D1 & n = (len <*(lower_bound A)*>) + i ) ;
consider j being Nat such that
A19: ( j in dom D1 & m = (len <*(lower_bound A)*>) + j ) by A4, A5, FINSEQ_1:38;
A20: i < j by A4, A18, A19, XREAL_1:8;
A21: D1 . i = (<*(lower_bound A)*> ^ D1) . n by A18, FINSEQ_1:def 7;
D1 . j = (<*(lower_bound A)*> ^ D1) . m by A19, FINSEQ_1:def 7;
hence (<*(lower_bound A)*> ^ D1) . n < (<*(lower_bound A)*> ^ D1) . m by A18, A19, A20, A21, SEQM_3:def 1; :: thesis: verum

end;

end;

end;

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

end;

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