let f be finite array; ( ( for a being Ordinal st a in dom f & succ a in dom f holds
f . (succ a) c< f . a ) implies f is descending )
assume A1:
for a being Ordinal st a in dom f & succ a in dom f holds
f . (succ a) c< f . a
; f is descending
let a be Ordinal; EXCHSORT:def 8 for b being Ordinal st a in dom f & b in dom f & a in b holds
f . b c< f . a
let b be Ordinal; ( a in dom f & b in dom f & a in b implies f . b c< f . a )
assume A2:
( a in dom f & b in dom f & a in b )
; f . b c< f . a
consider c, d being Ordinal such that
A3:
dom f = c \ d
by Def1;
consider n being Nat such that
A4:
c = d +^ n
by A2, A3, Th7;
consider e1 being Ordinal such that
A5:
( a = d +^ e1 & e1 in Segm n )
by A2, A3, A4, Th1;
consider e2 being Ordinal such that
A6:
( b = d +^ e2 & e2 in n )
by A2, A3, A4, Th1;
reconsider e1 = e1, e2 = e2 as Nat by A5, A6;
reconsider se1 = succ e1 as Element of NAT by ORDINAL1:def 12;
A7:
succ a = d +^ (succ e1)
by A5, ORDINAL2:28;
e1 in e2
by A2, A5, A6, ORDINAL3:22;
then
Segm (succ e1) c= Segm e2
by ORDINAL1:21;
then
succ e1 <= e2
by NAT_1:39;
then consider k being Nat such that
A8:
e2 = se1 + k
by NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
deffunc H1( Ordinal) -> set = (succ a) +^ $1;
defpred S9[ Nat] means ( H1($1) in dom f implies f . H1($1) c< f . a );
H1( 0 ) = succ a
by ORDINAL2:27;
then A9:
S9[ 0 ]
by A1, A2;
A10:
for k being Nat st S9[k] holds
S9[k + 1]
A16:
for k being Nat holds S9[k]
from NAT_1:sch 2(A9, A10);
b =
d +^ (se1 +^ k)
by A6, A8, CARD_2:36
.=
(succ a) +^ k
by A7, ORDINAL3:30
;
hence
f . b c< f . a
by A2, A16; verum