set F = idseq n;
let a be Nat; EUCLID_7:def 1 ( not 1 <= a or len (idseq n) <= a or not (idseq n) . (a + 1) <= (idseq n) . a )
assume that
A1:
1 <= a
and
A2:
a < len (idseq n)
; not (idseq n) . (a + 1) <= (idseq n) . a
a in Seg n
by A1, A2;
then A3:
(idseq n) . a = a
by FINSEQ_2:49;
A4:
1 <= a + 1
by NAT_1:11;
a + 1 <= n
by A2, NAT_1:13;
then A5:
a + 1 in Seg n
by A4;
a + 0 < a + 1
by XREAL_1:6;
hence
(idseq n) . a < (idseq n) . (a + 1)
by A3, A5, FINSEQ_2:49; verum