let O be non empty connected Poset; :: thesis: for R being array of O
for C being finite arr_computation of R holds
( last C is permutation of R & ( for a being ordinal number st a in dom C holds
C . a is permutation of R ) )
let R be array of O; :: thesis: for C being finite arr_computation of R holds
( last C is permutation of R & ( for a being ordinal number st a in dom C holds
C . a is permutation of R ) )
let C be finite arr_computation of R; :: thesis: ( last C is permutation of R & ( for a being ordinal number st a in dom C holds
C . a is permutation of R ) )
consider a, b being ordinal number such that
A0: dom C = a \ b by SEG;
consider n being natural number such that
A1: a = b +^ n by A0, Th009;
defpred S₉[ Nat] means ( b +^ $1 in dom C implies C . (b +^ $1) is permutation of R );
B1: b +^ 0 = b by ORDINAL2:27;
then n <> 0 by A0, A1, XBOOLE_1:37;
then consider m being Nat such that
B2: n = m + 1 by NAT_1:6;
B5: a = b +^ (succ m) by A1, B2, NAT_1:38
.= succ (b +^ m) by ORDINAL2:28 ;
then B4: b +^ m = union a by ORDINAL2:2
.= union (a \ b) by A0, Th008 ;
C . (base- C) = R by COMP;
then C . b = R by A0, Th011;
then A2: S₉[ 0 ] by B1, ThRef;
A3: for k being natural number st S₉[k] holds
S₉[k + 1]

proof

let k be natural number ; :: thesis: ( S₉[k] implies S₉[k + 1] )
assume C1: ( S₉[k] & b +^ (k + 1) in dom C ) ; :: thesis: C . (b +^ (k + 1)) is permutation of R
k + 1 = succ k by NAT_1:38;
then C2: b +^ (k + 1) = succ (b +^ k) by ORDINAL2:28;
then ( b +^ k in b +^ (k + 1) & b +^ (k + 1) in a ) by A0, C1, ORDINAL1:6;
then C3: ( b c= b +^ k & b +^ k in a ) by ORDINAL1:10, ORDINAL3:24;
then b +^ k in dom C by A0, ORDINAL6:5;
then consider Q being array of O, x, y being set such that
C4: ( [x,y] in inversions Q & C . (b +^ k) = Q & C . (b +^ (k + 1)) = Swap (Q,x,y) ) by C1, C2, COMP;
( x in dom Q & y in dom Q ) by C4, TW0;
then Swap (Q,x,y) is permutation of Q by Th13;
hence C . (b +^ (k + 1)) is permutation of R by C1, A0, C3, C4, ThTr, ORDINAL6:5; :: thesis: verum

end;

A4: for k being natural number holds S₉[k] from NAT_1:sch 2(A2, A3);
( b c= b +^ m & b +^ m in a ) by B5, ORDINAL1:6, ORDINAL3:24;
then ( S₉[m] & b +^ m in dom C ) by A0, A4, ORDINAL6:5;
hence last C is permutation of R by A0, B4; :: thesis: for a being ordinal number st a in dom C holds
C . a is permutation of R
let c be ordinal number ; :: thesis: ( c in dom C implies C . c is permutation of R )
assume A7: c in dom C ; :: thesis: C . c is permutation of R
then A5: ( b c= c & c in a ) by A0, ORDINAL6:5;
then c = b +^ (c -^ b) by ORDINAL3:def 5;
then c -^ b in n by A1, A7, A0, ORDINAL3:22;
then reconsider k = c -^ b as Nat ;
S₉[k] by A4;
hence C . c is permutation of R by A7, A5, ORDINAL3:def 5; :: thesis: verum