let f be finite array; :: thesis: ( ( for a being ordinal number st a in dom f & succ a in dom f holds
f . (succ a) c< f . a ) implies f is descending )
assume Z0: for a being ordinal number 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 number ; :: according to EXCHSORT:def 8 :: thesis: for b being ordinal number st a in dom f & b in dom f & a in b holds
f . b c< f . a
let b be ordinal number ; :: thesis: ( a in dom f & b in dom f & a in b implies f . b c< f . a )
assume Z1: ( a in dom f & b in dom f & a in b ) ; :: thesis: f . b c< f . a
consider c, d being ordinal number such that
A0: dom f = c \ d by SEG;
consider n being Nat such that
A1: c = d +^ n by Z1, A0, Th009;
consider e1 being Ordinal such that
01: ( a = d +^ e1 & e1 in n ) by Z1, A0, A1, OM1;
consider e2 being Ordinal such that
02: ( b = d +^ e2 & e2 in n ) by Z1, A0, A1, OM1;
reconsider e1 = e1, e2 = e2 as Nat by 01, 02;
reconsider se1 = succ e1 as Element of NAT by ORDINAL1:def 12;
03: succ a = d +^ (succ e1) by 01, ORDINAL2:28;
e1 in e2 by Z1, 01, 02, ORDINAL3:22;
then succ e1 c= e2 by ORDINAL1:21;
then succ e1 <= e2 by NAT_1:39;
then consider k being Nat such that
04: 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 A2: S₉[ 0 ] by Z0, Z1;
A3: for k being Nat st S₉[k] holds
S₉[k + 1]

proof

let k be Nat; :: thesis: ( S₉[k] implies S₉[k + 1] )
k + 1 = succ k by NAT_1:38;
then B2: H₁(k + 1) = succ H₁(k) by ORDINAL2:28;
then B3: ( H₁(k) in H₁(k + 1) & a in succ a ) by ORDINAL1:6;
then B5: ( H₁(k) c= H₁(k + 1) & a c= succ a ) by ORDINAL1:def 2;
succ a c= H₁(k) by ORDINAL3:24;
then B4: a c= H₁(k) by B3, ORDINAL1:def 2;
assume Z2: ( S₉[k] & H₁(k + 1) in dom f ) ; :: thesis: f . H₁(k + 1) c< f . a
then H₁(k) in dom f by Z1, B5, B4, OM2;
then ( f . H₁(k) c< f . a & f . H₁(k + 1) c< f . H₁(k) ) by Z0, B2, Z2;
hence f . H₁(k + 1) c< f . a by XBOOLE_1:56; :: thesis: verum

end;

A4: for k being Nat holds S₉[k] from NAT_1:sch 2(A2, A3);
b = d +^ (se1 +^ k) by 02, 04, CARD_2:36
.= (succ a) +^ k by 03, ORDINAL3:30 ;
hence f . b c< f . a by Z1, A4; :: thesis: verum