let O be non empty connected Poset; :: thesis: for R being array of O
for C being 0 -based arr_computation of R st R is finite array of O holds
C is finite
let R be array of O; :: thesis: for C being 0 -based arr_computation of R st R is finite array of O holds
C is finite
let C be 0 -based arr_computation of R; :: thesis: ( R is finite array of O implies C is finite )
assume R is finite array of O ; :: thesis: C is finite
then reconsider R = R as finite array of O ;
A1: C . (base- C) = R by Def14;
deffunc H₁( array of O) -> set = card (inversions $1);
base- C = 0 by Th24;
then A2: H₁(C . 0) is finite by A1;
A3: for a being Ordinal st succ a in dom C & H₁(C . a) is finite holds
H₁(C . (succ a)) c< H₁(C . a)

proof

let a be Ordinal; :: thesis: ( succ a in dom C & H₁(C . a) is finite implies H₁(C . (succ a)) c< H₁(C . a) )
assume A4: ( succ a in dom C & H₁(C . a) is finite ) ; :: thesis: H₁(C . (succ a)) c< H₁(C . a)
a in succ a by ORDINAL1:6;
then a in dom C by A4, ORDINAL1:10;
then consider R being array of O, x, y being set such that
A5: ( [x,y] in inversions R & C . a = R & C . (succ a) = Swap (R,x,y) ) by A4, Def14;
inversions R is finite by A4, A5;
then H₁(C . (succ a)) in H₁(C . a) by A5, Th73;
then ( H₁(C . (succ a)) c= H₁(C . a) & H₁(C . (succ a)) <> H₁(C . a) ) by ORDINAL1:def 2;
hence H₁(C . (succ a)) c< H₁(C . a) ; :: thesis: verum

end;

thus C is finite from EXCHSORT:sch 1(A2, A3); :: thesis: verum