let f be finite array; :: thesis: ( ( 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 ; :: thesis: f is descending
let a be Ordinal; :: according to EXCHSORT:def 8 :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: 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 H₁( Ordinal) -> set = (succ a) +^ $1;
defpred S₉[ Nat] means ( H₁($1) in dom f implies f . H₁($1) c< f . a );
H₁( 0 ) = succ a by ORDINAL2:27;
then A9: S₉[ 0 ] by A1, A2;
A10: for k being Nat st S₉[k] holds
S₉[k + 1]

proof

let k be Nat; :: thesis: ( S₉[k] implies S₉[k + 1] )
Segm (k + 1) = succ (Segm k) by NAT_1:38;
then A11: H₁(k + 1) = succ H₁(k) by ORDINAL2:28;
then A12: ( H₁(k) in H₁(k + 1) & a in succ a ) by ORDINAL1:6;
then A13: ( H₁(k) c= H₁(k + 1) & a c= succ a ) by ORDINAL1:def 2;
succ a c= H₁(k) by ORDINAL3:24;
then A14: a c= H₁(k) by A12, ORDINAL1:def 2;
assume A15: ( S₉[k] & H₁(k + 1) in dom f ) ; :: thesis: f . H₁(k + 1) c< f . a
then H₁(k) in dom f by A2, A13, A14, Th9;
then ( f . H₁(k) c< f . a & f . H₁(k + 1) c< f . H₁(k) ) by A1, A11, A15;
hence f . H₁(k + 1) c< f . a by XBOOLE_1:56; :: thesis: verum

end;

A16: for k being Nat holds S₉[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; :: thesis: verum