let f be array; ( len- f = omega & ( 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:
len- f = omega
; ( ex a being Ordinal st
( a in dom f & succ a in dom f & not f . (succ a) c< f . a ) or f is descending )
assume A2:
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 A3:
( a in dom f & b in dom f & a in b )
; f . b c< f . a
consider c, d being Ordinal such that
A4:
dom f = c \ d
by Def1;
not f is empty
by A3;
then A5:
( base- f = d & limit- f = c )
by A4, Th23;
( d c= a & a in c )
by A3, A4, ORDINAL6:5;
then
d in c
by ORDINAL1:12;
then
d c= c
by ORDINAL1:def 2;
then A6:
c = d +^ omega
by A5, A1, ORDINAL3:def 5;
consider e1 being Ordinal such that
A7:
( a = d +^ e1 & e1 in omega )
by A3, A4, A6, Th1;
consider e2 being Ordinal such that
A8:
( b = d +^ e2 & e2 in omega )
by A3, A4, A6, Th1;
reconsider e1 = e1, e2 = e2 as Nat by A7, A8;
reconsider se1 = succ e1 as Element of NAT by ORDINAL1:def 12;
A9:
succ a = d +^ (succ e1)
by A7, ORDINAL2:28;
e1 in e2
by A3, A7, A8, 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
A10:
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 A11:
S9[ 0 ]
by A2, A3;
A12:
for k being Nat st S9[k] holds
S9[k + 1]
A18:
for k being Nat holds S9[k]
from NAT_1:sch 2(A11, A12);
b =
d +^ (se1 +^ k)
by A8, A10, CARD_2:36
.=
(succ a) +^ k
by A9, ORDINAL3:30
;
hence
f . b c< f . a
by A3, A18; verum