:: EXCHSORT semantic presentation

begin


theorem Th1: :: EXCHSORT:1
for a, b being ordinal number
for x being set holds
( x in (a +^ b) \ a iff ex c being ordinal number st
( x = a +^ c & c in b ) )
proof
let a, b be ordinal number ; ::_thesis: for x being set holds
( x in (a +^ b) \ a iff ex c being ordinal number st
( x = a +^ c & c in b ) )
let x be set ; ::_thesis: ( x in (a +^ b) \ a iff ex c being ordinal number st
( x = a +^ c & c in b ) )
A1: ( x in (a +^ b) \ a iff ( a c= x & x in a +^ b ) ) by ORDINAL6:5;
hereby  ::_thesis: ( ex c being ordinal number st
( x = a +^ c & c in b ) implies x in (a +^ b) \ a )
assume A2: x in (a +^ b) \ a ; ::_thesis: ex d being set st
( x = a +^ d & d in b )
then reconsider c = x as Ordinal ;
take d = c -^ a; ::_thesis: ( x = a +^ d & d in b )
thus  x = a +^ d by A1, A2, ORDINAL3:def_5; ::_thesis: d in b
hence  d in b by A2, ORDINAL3:22; ::_thesis: verum
end;
given c being ordinal number  such that A3: ( x = a +^ c & c in b ) ; ::_thesis: x in (a +^ b) \ a
 ( a c= x & x in a +^ b ) by A3, ORDINAL2:32, ORDINAL3:24;
hence  x in (a +^ b) \ a by ORDINAL6:5; ::_thesis: verum
end;

defpred S1[ set , set , set , set ] means ( $3 <> $1 & $3 <> $2 & $4 <> $1 & $4 <> $2 );

defpred S2[ set , set , set , set ] means ( $3 in $1 & $4 = $1 );

defpred S3[ set , set , set , set ] means ( $3 in $1 & $4 = $2 );

defpred S4[ set , set , set , set ] means ( $3 = $1 & $4 in $2 );

defpred S5[ set , set , set , set ] means ( $3 = $1 & $4 = $2 );

defpred S6[ set , set , set , set ] means ( $3 = $1 & $2 in $4 );

defpred S7[ set , set , set , set ] means ( $1 in $3 & $4 = $2 );

defpred S8[ set , set , set , set ] means ( $3 = $2 & $2 in $4 );

theorem Th2: :: EXCHSORT:2
for a, b, c, d being ordinal number st a in b & c in d & not ( c <> a & c <> b & d <> a & d <> b ) & not ( c in a & d = a ) & not ( c in a & d = b ) & not ( c = a & d in b ) & not ( c = a & d = b ) & not ( c = a & b in d ) & not ( a in c & d = b ) holds
( c = b & b in d )
proof
let a, b, c, d be ordinal number ; ::_thesis: ( a in b & c in d & not ( c <> a & c <> b & d <> a & d <> b ) & not ( c in a & d = a ) & not ( c in a & d = b ) & not ( c = a & d in b ) & not ( c = a & d = b ) & not ( c = a & b in d ) & not ( a in c & d = b ) implies ( c = b & b in d ) )
assume A1: ( a in b & c in d ) ; ::_thesis: ( ( c <> a & c <> b & d <> a & d <> b ) or ( c in a & d = a ) or ( c in a & d = b ) or ( c = a & d in b ) or ( c = a & d = b ) or ( c = a & b in d ) or ( a in c & d = b ) or ( c = b & b in d ) )
percases ( c in a or c = a or ( a in c & c in b ) or c = b or b in c ) by ORDINAL1:14;
suppose c in a ; ::_thesis: ( ( c <> a & c <> b & d <> a & d <> b ) or ( c in a & d = a ) or ( c in a & d = b ) or ( c = a & d in b ) or ( c = a & d = b ) or ( c = a & b in d ) or ( a in c & d = b ) or ( c = b & b in d ) )
hence  ( ( c <> a & c <> b & d <> a & d <> b ) or ( c in a & d = a ) or ( c in a & d = b ) or ( c = a & d in b ) or ( c = a & d = b ) or ( c = a & b in d ) or ( a in c & d = b ) or ( c = b & b in d ) ) by A1; ::_thesis: verum
end;
suppose c = a ; ::_thesis: ( ( c <> a & c <> b & d <> a & d <> b ) or ( c in a & d = a ) or ( c in a & d = b ) or ( c = a & d in b ) or ( c = a & d = b ) or ( c = a & b in d ) or ( a in c & d = b ) or ( c = b & b in d ) )
hence  ( ( c <> a & c <> b & d <> a & d <> b ) or ( c in a & d = a ) or ( c in a & d = b ) or ( c = a & d in b ) or ( c = a & d = b ) or ( c = a & b in d ) or ( a in c & d = b ) or ( c = b & b in d ) ) by ORDINAL1:14; ::_thesis: verum
end;
supposeA2: ( a in c & c in b ) ; ::_thesis: ( ( c <> a & c <> b & d <> a & d <> b ) or ( c in a & d = a ) or ( c in a & d = b ) or ( c = a & d in b ) or ( c = a & d = b ) or ( c = a & b in d ) or ( a in c & d = b ) or ( c = b & b in d ) )
percases ( d in b or d = b or b in d ) by ORDINAL1:14;
suppose d in b ; ::_thesis: ( ( c <> a & c <> b & d <> a & d <> b ) or ( c in a & d = a ) or ( c in a & d = b ) or ( c = a & d in b ) or ( c = a & d = b ) or ( c = a & b in d ) or ( a in c & d = b ) or ( c = b & b in d ) )
hence  ( ( c <> a & c <> b & d <> a & d <> b ) or ( c in a & d = a ) or ( c in a & d = b ) or ( c = a & d in b ) or ( c = a & d = b ) or ( c = a & b in d ) or ( a in c & d = b ) or ( c = b & b in d ) ) by A1; ::_thesis: verum
end;
suppose d = b ; ::_thesis: ( ( c <> a & c <> b & d <> a & d <> b ) or ( c in a & d = a ) or ( c in a & d = b ) or ( c = a & d in b ) or ( c = a & d = b ) or ( c = a & b in d ) or ( a in c & d = b ) or ( c = b & b in d ) )
hence  ( ( c <> a & c <> b & d <> a & d <> b ) or ( c in a & d = a ) or ( c in a & d = b ) or ( c = a & d in b ) or ( c = a & d = b ) or ( c = a & b in d ) or ( a in c & d = b ) or ( c = b & b in d ) ) by A2; ::_thesis: verum
end;
suppose b in d ; ::_thesis: ( ( c <> a & c <> b & d <> a & d <> b ) or ( c in a & d = a ) or ( c in a & d = b ) or ( c = a & d in b ) or ( c = a & d = b ) or ( c = a & b in d ) or ( a in c & d = b ) or ( c = b & b in d ) )
hence  ( ( c <> a & c <> b & d <> a & d <> b ) or ( c in a & d = a ) or ( c in a & d = b ) or ( c = a & d in b ) or ( c = a & d = b ) or ( c = a & b in d ) or ( a in c & d = b ) or ( c = b & b in d ) ) by A1; ::_thesis: verum
end;
end;
end;
suppose c = b ; ::_thesis: ( ( c <> a & c <> b & d <> a & d <> b ) or ( c in a & d = a ) or ( c in a & d = b ) or ( c = a & d in b ) or ( c = a & d = b ) or ( c = a & b in d ) or ( a in c & d = b ) or ( c = b & b in d ) )
hence  ( ( c <> a & c <> b & d <> a & d <> b ) or ( c in a & d = a ) or ( c in a & d = b ) or ( c = a & d in b ) or ( c = a & d = b ) or ( c = a & b in d ) or ( a in c & d = b ) or ( c = b & b in d ) ) by A1; ::_thesis: verum
end;
suppose b in c ; ::_thesis: ( ( c <> a & c <> b & d <> a & d <> b ) or ( c in a & d = a ) or ( c in a & d = b ) or ( c = a & d in b ) or ( c = a & d = b ) or ( c = a & b in d ) or ( a in c & d = b ) or ( c = b & b in d ) )
hence  ( ( c <> a & c <> b & d <> a & d <> b ) or ( c in a & d = a ) or ( c in a & d = b ) or ( c = a & d in b ) or ( c = a & d = b ) or ( c = a & b in d ) or ( a in c & d = b ) or ( c = b & b in d ) ) by A1; ::_thesis: verum
end;
end;
end;

theorem :: EXCHSORT:3
for x, y being set st x nin y holds
(y \/ {x}) \ y = {x} by XBOOLE_1:88, ZFMISC_1:50;

theorem Th4: :: EXCHSORT:4
for x being set holds (succ x) \ x = {x}
proof
let x be set ; ::_thesis: (succ x) \ x = {x}
 ( succ x = x \/ {x} & x nin x ) ;
hence  (succ x) \ x = {x} by XBOOLE_1:88, ZFMISC_1:50; ::_thesis: verum
end;

theorem Th5: :: EXCHSORT:5
for f being Function
for r being Relation
for x being set holds
( x in f .: r iff ex y, z being set st
( [y,z] in r & [y,z] in dom f & f . (y,z) = x ) )
proof
let f be Function; ::_thesis: for r being Relation
for x being set holds
( x in f .: r iff ex y, z being set st
( [y,z] in r & [y,z] in dom f & f . (y,z) = x ) )
let r be Relation; ::_thesis: for x being set holds
( x in f .: r iff ex y, z being set st
( [y,z] in r & [y,z] in dom f & f . (y,z) = x ) )
let x be set ; ::_thesis: ( x in f .: r iff ex y, z being set st
( [y,z] in r & [y,z] in dom f & f . (y,z) = x ) )
hereby  ::_thesis: ( ex y, z being set st
( [y,z] in r & [y,z] in dom f & f . (y,z) = x ) implies x in f .: r )
assume  x in f .: r ; ::_thesis: ex y, z being set st
( [y,z] in r & [y,z] in dom f & f . (y,z) = x )
then consider t being set  such that
A1: ( t in dom f & t in r & x = f . t ) by FUNCT_1:def_6;
consider y, z being set  such that
A2: t = [y,z] by A1, RELAT_1:def_1;
 f . (y,z) = f . [y,z] ;
hence  ex y, z being set st
( [y,z] in r & [y,z] in dom f & f . (y,z) = x ) by A1, A2; ::_thesis: verum
end;
thus  ( ex y, z being set st
( [y,z] in r & [y,z] in dom f & f . (y,z) = x ) implies x in f .: r ) by FUNCT_1:def_6; ::_thesis: verum
end;

theorem Th6: :: EXCHSORT:6
for a, b being ordinal number st a \ b <> {} holds
( inf (a \ b) = b & sup (a \ b) = a & union (a \ b) = union a )
proof
let a, b be ordinal number ; ::_thesis: ( a \ b <> {} implies ( inf (a \ b) = b & sup (a \ b) = a & union (a \ b) = union a ) )
assume A1: a \ b <> {} ; ::_thesis: ( inf (a \ b) = b & sup (a \ b) = a & union (a \ b) = union a )
set x = the Element of a \ b;
A2: the Element of a \ b in a \ b by A1;
A3: ( the Element of a \ b in a & the Element of a \ b nin b ) by A1, XBOOLE_0:def_5;
then  b c= the Element of a \ b by ORDINAL6:4;
then  ( b in a & b nin b ) by A3, ORDINAL1:12;
then A4: b in a \ b by XBOOLE_0:def_5;
hence  inf (a \ b) c= b by ORDINAL2:14; :: according to XBOOLE_0:def_10 ::_thesis: ( b c= inf (a \ b) & sup (a \ b) = a & union (a \ b) = union a )
 inf (a \ b) in a \ b by A2, ORDINAL2:17;
then  inf (a \ b) nin b by XBOOLE_0:def_5;
hence  b c= inf (a \ b) by ORDINAL6:4; ::_thesis: ( sup (a \ b) = a & union (a \ b) = union a )
A5: On (a \ b) = a \ b by ORDINAL6:2;
thus  sup (a \ b) c= a by A5, ORDINAL2:def_3; :: according to XBOOLE_0:def_10 ::_thesis: ( a c= sup (a \ b) & union (a \ b) = union a )
thus  a c= sup (a \ b) ::_thesis: union (a \ b) = union a
proof
let c be ordinal number ; :: according to ORDINAL1:def_5 ::_thesis: ( not c in a or c in sup (a \ b) )
assume A6: c in a ; ::_thesis: c in sup (a \ b)
A7: b in sup (a \ b) by A4, ORDINAL2:19;
percases ( c in b or c nin b ) ;
suppose c in b ; ::_thesis: c in sup (a \ b)
hence  c in sup (a \ b) by A7, ORDINAL1:10; ::_thesis: verum
end;
suppose c nin b ; ::_thesis: c in sup (a \ b)
then  c in a \ b by A6, XBOOLE_0:def_5;
hence  c in sup (a \ b) by ORDINAL2:19; ::_thesis: verum
end;
end;
end;
thus  union (a \ b) c= union a by ZFMISC_1:77; :: according to XBOOLE_0:def_10 ::_thesis: union a c= union (a \ b)
 for y being set st y in union a holds
y in union (a \ b)
proof
let y be set ; ::_thesis: ( y in union a implies y in union (a \ b) )
assume  y in union a ; ::_thesis: y in union (a \ b)
then consider x being set  such that
A8: ( y in x & x in a ) by TARSKI:def_4;
reconsider x = x as Ordinal by A8;
percases ( x in b or b c= x ) by ORDINAL6:4;
suppose x in b ; ::_thesis: y in union (a \ b)
then  y in b by A8, ORDINAL1:10;
hence  y in union (a \ b) by A4, TARSKI:def_4; ::_thesis: verum
end;
suppose b c= x ; ::_thesis: y in union (a \ b)
then  x in a \ b by A8, ORDINAL6:5;
hence  y in union (a \ b) by A8, TARSKI:def_4; ::_thesis: verum
end;
end;
end;
hence  union a c= union (a \ b) by TARSKI:def_3; ::_thesis: verum
end;

theorem Th7: :: EXCHSORT:7
for a, b being ordinal number st not a \ b is empty & a \ b is finite holds
ex n being Nat st a = b +^ n
proof
let a, b be ordinal number ; ::_thesis: ( not a \ b is empty & a \ b is finite implies ex n being Nat st a = b +^ n )
assume A1: ( not a \ b is empty & a \ b is finite ) ; ::_thesis: ex n being Nat st a = b +^ n
set x = the Element of a \ b;
A2: ( the Element of a \ b in a & the Element of a \ b nin b ) by A1, XBOOLE_0:def_5;
then  b c= the Element of a \ b by ORDINAL6:4;
then consider c being ordinal number  such that
A3: ( a = b +^ c & c <> {} ) by A2, ORDINAL1:12, ORDINAL3:28;
deffunc H1( Ordinal) ->  set = b +^ $1;
consider f being T-Sequence such that
A4: ( dom f = omega & ( for d being ordinal number st d in omega holds
f . d = H1(d) ) ) from ORDINAL2:sch_2();
 f is one-to-one
proof
let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not x in proj1 f or not b1 in proj1 f or not f . x = f . b1 or x = b1 )
let y be set ; ::_thesis: ( not x in proj1 f or not y in proj1 f or not f . x = f . y or x = y )
assume A5: ( x in dom f & y in dom f & f . x = f . y & x <> y ) ; ::_thesis: contradiction
then reconsider x = x, y = y as Element of omega by A4;
A6: ( f . x = H1(x) & f . y = H1(y) ) by A4;
 ( x in y or y in x ) by A5, ORDINAL1:14;
then  ( b +^ x in b +^ y or b +^ y in b +^ x ) by ORDINAL2:32;
hence  contradiction by A5, A6; ::_thesis: verum
end;
then A7: omega , rng f are_equipotent by A4, WELLORD2:def_4;
now__::_thesis:_not_omega_c=_c
assume  omega c= c ; ::_thesis: contradiction
then A8: H1( omega ) c= a by A3, ORDINAL2:33;
 rng f c= a \ b
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in a \ b )
assume  y in rng f ; ::_thesis: y in a \ b
then consider x being set  such that
A9: ( x in dom f & y = f . x ) by FUNCT_1:def_3;
reconsider x = x as Element of omega by A4, A9;
A10: y = H1(x) by A4, A9;
 ( b c= H1(x) & H1(x) in H1( omega ) ) by ORDINAL2:32, ORDINAL3:24;
then  ( y nin b & y in a ) by A8, A10, ORDINAL6:4;
hence  y in a \ b by XBOOLE_0:def_5; ::_thesis: verum
end;
hence  contradiction by A1, A7, CARD_1:38; ::_thesis: verum
end;
then  c in omega by ORDINAL6:4;
hence  ex n being Nat st a = b +^ n by A3; ::_thesis: verum
end;

begin

definition
let f be set ;
attrf is segmental  means :Def1: :: EXCHSORT:def 1
 ex a, b being ordinal number st proj1 f = a \ b;
end;

:: deftheorem Def1 defines segmental EXCHSORT:def_1_:_
 for f being set holds
( f is segmental iff ex a, b being ordinal number st proj1 f = a \ b );


theorem :: EXCHSORT:8
for f, g being Function st dom f = dom g & f is segmental holds
g is segmental
proof
let f, g be Function; ::_thesis: ( dom f = dom g & f is segmental implies g is segmental )
assume A1: dom f = dom g ; ::_thesis: ( not f is segmental or g is segmental )
given a, b being ordinal number  such that A2: dom f = a \ b ; :: according to EXCHSORT:def_1 ::_thesis: g is segmental
take  a ; :: according to EXCHSORT:def_1 ::_thesis: ex b being ordinal number st proj1 g = a \ b
take  b ; ::_thesis: proj1 g = a \ b
thus  proj1 g = a \ b by A1, A2; ::_thesis: verum
end;

theorem Th9: :: EXCHSORT:9
for f being Function st f is segmental holds
for a, b, c being ordinal number st a c= b & b c= c & a in dom f & c in dom f holds
b in dom f
proof
let f be Function; ::_thesis: ( f is segmental implies for a, b, c being ordinal number st a c= b & b c= c & a in dom f & c in dom f holds
b in dom f )
given x, y being Ordinal such that A1: dom f = x \ y ; :: according to EXCHSORT:def_1 ::_thesis: for a, b, c being ordinal number st a c= b & b c= c & a in dom f & c in dom f holds
b in dom f
let a, b, c be ordinal number ; ::_thesis: ( a c= b & b c= c & a in dom f & c in dom f implies b in dom f )
assume A2: ( a c= b & b c= c & a in dom f & c in dom f ) ; ::_thesis: b in dom f
then  ( y c= a & c in x ) by A1, ORDINAL6:5;
then  ( y c= b & b in x ) by A2, ORDINAL1:12, XBOOLE_1:1;
hence  b in dom f by A1, ORDINAL6:5; ::_thesis: verum
end;

registration
cluster T-Sequence-like Relation-like Function-like  ->  segmental for set ;
coherence
 for b1 being Function st b1 is T-Sequence-like holds
b1 is segmental
proof
let f be Function; ::_thesis: ( f is T-Sequence-like implies f is segmental )
assume  f is T-Sequence-like ; ::_thesis: f is segmental
then reconsider f = f as T-Sequence ;
take  dom f ; :: according to EXCHSORT:def_1 ::_thesis: ex b being ordinal number st proj1 f = (dom f) \ b
take  0 ; ::_thesis: proj1 f = (dom f) \ 0
thus  proj1 f = (dom f) \ 0 ; ::_thesis: verum
end;
cluster Relation-like Function-like FinSequence-like  ->  segmental for set ;
coherence
 for b1 being Function st b1 is FinSequence-like holds
b1 is segmental
proof
let f be Function; ::_thesis: ( f is FinSequence-like implies f is segmental )
assume  f is FinSequence-like ; ::_thesis: f is segmental
then reconsider g = f as FinSequence ;
take a = succ (len g); :: according to EXCHSORT:def_1 ::_thesis: ex b being ordinal number st proj1 f = a \ b
take b = 1; ::_thesis: proj1 f = a \ b
reconsider c = len g as Nat ;
thus  dom f c= a \ b :: according to XBOOLE_0:def_10 ::_thesis: a \ b c= proj1 f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom f or x in a \ b )
assume A1: x in dom f ; ::_thesis: x in a \ b
then  x in dom g ;
then reconsider x = x as Nat ;
 x <= c by A1, FINSEQ_3:25;
then A2: ( 1 <= x & x <= c ) by A1, FINSEQ_3:25;
then  ( succ 0 c= x & x c= c ) by NAT_1:39;
then A3: ( 0 in x & x in a ) by ORDINAL1:21, ORDINAL1:22;
 not x in b by A2, CARD_1:49, TARSKI:def_1;
hence  x in a \ b by A3, XBOOLE_0:def_5; ::_thesis: verum
end;
reconsider d = a as Element of NAT by ORDINAL1:def_12;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in a \ b or x in proj1 f )
assume A4: x in a \ b ; ::_thesis: x in proj1 f
then A5: ( x in d & not x in b ) by XBOOLE_0:def_5;
reconsider x = x as Nat by A4;
 ( x c= c & b c= x ) by A5, ORDINAL1:16, ORDINAL1:22;
then  ( 1 <= x & x <= c ) by NAT_1:39;
hence  x in proj1 f by FINSEQ_3:25; ::_thesis: verum
end;
end;

definition
let a be ordinal number ;
let s be set ;
attrs is a -based  means :Def2: :: EXCHSORT:def 2
 for b being ordinal number st b in proj1 s holds
( a in proj1 s & a c= b );
attrs is a -limited  means :Def3: :: EXCHSORT:def 3
a = sup (proj1 s);
end;

:: deftheorem Def2 defines -based EXCHSORT:def_2_:_
 for a being ordinal number
for s being set holds
( s is a -based iff for b being ordinal number st b in proj1 s holds
( a in proj1 s & a c= b ) );

:: deftheorem Def3 defines -limited EXCHSORT:def_3_:_
 for a being ordinal number
for s being set holds
( s is a -limited iff a = sup (proj1 s) );

theorem :: EXCHSORT:10
for a being ordinal number
for f being Function holds
( ( f is a -based & f is segmental ) iff ex b being ordinal number st
( dom f = b \ a & a c= b ) )
proof
let a be ordinal number ; ::_thesis: for f being Function holds
( ( f is a -based & f is segmental ) iff ex b being ordinal number st
( dom f = b \ a & a c= b ) )
let f be Function; ::_thesis: ( ( f is a -based & f is segmental ) iff ex b being ordinal number st
( dom f = b \ a & a c= b ) )
thus  ( f is a -based & f is segmental implies ex b being ordinal number st
( dom f = b \ a & a c= b ) ) ::_thesis: ( ex b being ordinal number st
( dom f = b \ a & a c= b ) implies ( f is a -based & f is segmental ) )
proof
assume A1: for b being ordinal number st b in dom f holds
( a in dom f & a c= b ) ; :: according to EXCHSORT:def_2 ::_thesis: ( not f is segmental or ex b being ordinal number st
( dom f = b \ a & a c= b ) )
given c, d being ordinal number  such that A2: dom f = c \ d ; :: according to EXCHSORT:def_1 ::_thesis: ex b being ordinal number st
( dom f = b \ a & a c= b )
set x = the Element of c \ d;
percases ( dom f = {} or dom f <> {} ) ;
suppose dom f = {} ; ::_thesis: ex b being ordinal number st
( dom f = b \ a & a c= b )
then  a \ a = dom f by XBOOLE_1:37;
hence  ex b being ordinal number st
( dom f = b \ a & a c= b ) ; ::_thesis: verum
end;
suppose dom f <> {} ; ::_thesis: ex b being ordinal number st
( dom f = b \ a & a c= b )
then  the Element of c \ d in dom f by A2;
then  a in dom f by A1;
then A3: ( d c= a & a in c ) by A2, ORDINAL6:5;
then  d in c by ORDINAL1:12;
then  d in dom f by A2, ORDINAL6:5;
then  a c= d by A1;
then  ( a = d & a c= c ) by A3, ORDINAL1:def_2, XBOOLE_0:def_10;
hence  ex b being ordinal number st
( dom f = b \ a & a c= b ) by A2; ::_thesis: verum
end;
end;
end;
given b being ordinal number  such that A4: ( dom f = b \ a & a c= b ) ; ::_thesis: ( f is a -based & f is segmental )
thus  f is a -based ::_thesis: f is segmental
proof
let c be ordinal number ; :: according to EXCHSORT:def_2 ::_thesis: ( c in proj1 f implies ( a in proj1 f & a c= c ) )
assume A5: c in dom f ; ::_thesis: ( a in proj1 f & a c= c )
then  ( a c= c & c in b ) by A4, ORDINAL6:5;
then  a in b by ORDINAL1:12;
hence  ( a in proj1 f & a c= c ) by A4, A5, ORDINAL6:5; ::_thesis: verum
end;
take  b ; :: according to EXCHSORT:def_1 ::_thesis: ex b being ordinal number st proj1 f = b \ b
take  a ; ::_thesis: proj1 f = b \ a
thus  proj1 f = b \ a by A4; ::_thesis: verum
end;

theorem :: EXCHSORT:11
for b being ordinal number
for f being Function holds
( ( f is b -limited & not f is empty & f is segmental ) iff ex a being ordinal number st
( dom f = b \ a & a in b ) )
proof
let b be ordinal number ; ::_thesis: for f being Function holds
( ( f is b -limited & not f is empty & f is segmental ) iff ex a being ordinal number st
( dom f = b \ a & a in b ) )
let f be Function; ::_thesis: ( ( f is b -limited & not f is empty & f is segmental ) iff ex a being ordinal number st
( dom f = b \ a & a in b ) )
thus  ( f is b -limited & not f is empty & f is segmental implies ex a being ordinal number st
( dom f = b \ a & a in b ) ) ::_thesis: ( ex a being ordinal number st
( dom f = b \ a & a in b ) implies ( f is b -limited & not f is empty & f is segmental ) )
proof
assume A1: b = sup (dom f) ; :: according to EXCHSORT:def_3 ::_thesis: ( f is empty or not f is segmental or ex a being ordinal number st
( dom f = b \ a & a in b ) )
assume A2: not f is empty ; ::_thesis: ( not f is segmental or ex a being ordinal number st
( dom f = b \ a & a in b ) )
given c, d being ordinal number  such that A3: dom f = c \ d ; :: according to EXCHSORT:def_1 ::_thesis: ex a being ordinal number st
( dom f = b \ a & a in b )
set x = the Element of c \ d;
take a = d; ::_thesis: ( dom f = b \ a & a in b )
A4: b = c by A2, A1, A3, Th6;
thus  dom f = b \ a by A2, A1, A3, Th6; ::_thesis: a in b
 ( a c= the Element of c \ d & the Element of c \ d in b ) by A2, A3, A4, ORDINAL6:5;
hence  a in b by ORDINAL1:12; ::_thesis: verum
end;
given a being ordinal number  such that A5: ( dom f = b \ a & a in b ) ; ::_thesis: ( f is b -limited & not f is empty & f is segmental )
 a in dom f by A5, ORDINAL6:5;
hence  b = sup (dom f) by A5, Th6; :: according to EXCHSORT:def_3 ::_thesis: ( not f is empty & f is segmental )
thus  not f is empty by A5, ORDINAL6:5; ::_thesis: f is segmental
take  b ; :: according to EXCHSORT:def_1 ::_thesis: ex b being ordinal number st proj1 f = b \ b
take  a ; ::_thesis: proj1 f = b \ a
thus  proj1 f = b \ a by A5; ::_thesis: verum
end;

registration
cluster T-Sequence-like Relation-like Function-like  ->  0 -based for set ;
coherence
 for b1 being Function st b1 is T-Sequence-like holds
b1 is 0 -based
proof
let f be Function; ::_thesis: ( f is T-Sequence-like implies f is 0 -based )
assume  f is T-Sequence-like ; ::_thesis: f is 0 -based
then reconsider g = f as T-Sequence ;
let b be ordinal number ; :: according to EXCHSORT:def_2 ::_thesis: ( b in proj1 f implies ( 0 in proj1 f & 0 c= b ) )
assume  b in dom f ; ::_thesis: ( 0 in proj1 f & 0 c= b )
then  b in dom g ;
hence  ( 0 in proj1 f & 0 c= b ) by ORDINAL3:8; ::_thesis: verum
end;
cluster Relation-like Function-like FinSequence-like  -> 1 -based for set ;
coherence
 for b1 being Function st b1 is FinSequence-like holds
b1 is 1 -based
proof
let f be Function; ::_thesis: ( f is FinSequence-like implies f is 1 -based )
assume  f is FinSequence-like ; ::_thesis: f is 1 -based
then reconsider g = f as FinSequence ;
let b be ordinal number ; :: according to EXCHSORT:def_2 ::_thesis: ( b in proj1 f implies ( 1 in proj1 f & 1 c= b ) )
assume  b in dom f ; ::_thesis: ( 1 in proj1 f & 1 c= b )
then A1: b in dom g ;
then reconsider b = b as Nat ;
A2: ( 1 <= b & b <= len g ) by A1, FINSEQ_3:25;
then  1 <= len g by XXREAL_0:2;
hence  ( 1 in proj1 f & 1 c= b ) by A2, FINSEQ_3:25, NAT_1:39; ::_thesis: verum
end;
end;

theorem Th12: :: EXCHSORT:12
for f being Function holds f is inf (dom f) -based
proof
let f be Function; ::_thesis: f is inf (dom f) -based
set b = inf (dom f);
let c be ordinal number ; :: according to EXCHSORT:def_2 ::_thesis: ( c in proj1 f implies ( inf (dom f) in proj1 f & inf (dom f) c= c ) )
assume  c in dom f ; ::_thesis: ( inf (dom f) in proj1 f & inf (dom f) c= c )
hence  ( inf (dom f) in dom f & inf (dom f) c= c ) by ORDINAL2:14, ORDINAL2:17; ::_thesis: verum
end;

theorem :: EXCHSORT:13
for f being Function holds f is sup (dom f) -limited by Def3;

theorem :: EXCHSORT:14
for b, a being ordinal number
for f being Function st f is b -limited & a in dom f holds
a in b
proof
let b, a be ordinal number ; ::_thesis: for f being Function st f is b -limited & a in dom f holds
a in b
let f be Function; ::_thesis: ( f is b -limited & a in dom f implies a in b )
assume  b = sup (dom f) ; :: according to EXCHSORT:def_3 ::_thesis: ( not a in dom f or a in b )
hence  ( not a in dom f or a in b ) by ORDINAL2:19; ::_thesis: verum
end;

definition
let f be Function;
func base- f ->  ordinal number  means :Def4: :: EXCHSORT:def 4
f is it -based  if  ex a being ordinal number st a in dom f
otherwise it = 0 ;
existence
 ( ( ex a being ordinal number st a in dom f implies ex b1 being ordinal number st f is b1 -based ) & ( ( for a being ordinal number holds not a in dom f ) implies ex b1 being ordinal number st b1 = 0 ) )
proof
set b = inf (dom f);
hereby  ::_thesis: ( ( for a being ordinal number holds not a in dom f ) implies ex b1 being ordinal number st b1 = 0 )
given a being ordinal number  such that  a in dom f ; ::_thesis: ex b being set st f is b -based
take b = inf (dom f); ::_thesis: f is b -based
thus  f is b -based by Th12; ::_thesis: verum
end;
assume  for a being ordinal number holds not a in dom f ; ::_thesis: ex b1 being ordinal number st b1 = 0
take  0 ; ::_thesis: 0 = 0
thus  0 = 0 ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being ordinal number holds
( ( ex a being ordinal number st a in dom f & f is b1 -based & f is b2 -based implies b1 = b2 ) & ( ( for a being ordinal number holds not a in dom f ) & b1 = 0 & b2 = 0 implies b1 = b2 ) )
proof
let b, c be ordinal number ; ::_thesis: ( ( ex a being ordinal number st a in dom f & f is b -based & f is c -based implies b = c ) & ( ( for a being ordinal number holds not a in dom f ) & b = 0 & c = 0 implies b = c ) )
hereby  ::_thesis: ( ( for a being ordinal number holds not a in dom f ) & b = 0 & c = 0 implies b = c )
given a being ordinal number  such that A1: a in dom f ; ::_thesis: ( f is b -based & f is c -based implies b = c )
assume A2: ( f is b -based & f is c -based ) ; ::_thesis: b = c
thus  b = c ::_thesis: verum
proof
 c in dom f by A1, A2, Def2;
hence  b c= c by A2, Def2; :: according to XBOOLE_0:def_10 ::_thesis: c c= b
 b in dom f by A1, A2, Def2;
hence  c c= b by A2, Def2; ::_thesis: verum
end;
end;
thus  ( ( for a being ordinal number holds not a in dom f ) & b = 0 & c = 0 implies b = c ) ; ::_thesis: verum
end;
consistency
 for b1 being ordinal number holds verum ;
func limit- f ->  ordinal number  means :Def5: :: EXCHSORT:def 5
f is it -limited  if  ex a being ordinal number st a in dom f
otherwise it = 0 ;
existence
 ( ( ex a being ordinal number st a in dom f implies ex b1 being ordinal number st f is b1 -limited ) & ( ( for a being ordinal number holds not a in dom f ) implies ex b1 being ordinal number st b1 = 0 ) )
proof
set b = sup (dom f);
hereby  ::_thesis: ( ( for a being ordinal number holds not a in dom f ) implies ex b1 being ordinal number st b1 = 0 )
given a being ordinal number  such that  a in dom f ; ::_thesis: ex b being set st f is b -limited
take b = sup (dom f); ::_thesis: f is b -limited
thus  f is b -limited by Def3; ::_thesis: verum
end;
assume  for a being ordinal number holds not a in dom f ; ::_thesis: ex b1 being ordinal number st b1 = 0
take  0 ; ::_thesis: 0 = 0
thus  0 = 0 ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being ordinal number holds
( ( ex a being ordinal number st a in dom f & f is b1 -limited & f is b2 -limited implies b1 = b2 ) & ( ( for a being ordinal number holds not a in dom f ) & b1 = 0 & b2 = 0 implies b1 = b2 ) )
proof
let b, c be ordinal number ; ::_thesis: ( ( ex a being ordinal number st a in dom f & f is b -limited & f is c -limited implies b = c ) & ( ( for a being ordinal number holds not a in dom f ) & b = 0 & c = 0 implies b = c ) )
hereby  ::_thesis: ( ( for a being ordinal number holds not a in dom f ) & b = 0 & c = 0 implies b = c )
given a being ordinal number  such that  a in dom f ; ::_thesis: ( f is b -limited & f is c -limited implies b = c )
assume A3: ( f is b -limited & f is c -limited ) ; ::_thesis: b = c
thus b = sup (dom f) by A3, Def3
.= c by A3, Def3 ; ::_thesis: verum
end;
thus  ( ( for a being ordinal number holds not a in dom f ) & b = 0 & c = 0 implies b = c ) ; ::_thesis: verum
end;
consistency
 for b1 being ordinal number holds verum ;
end;

:: deftheorem Def4 defines base- EXCHSORT:def_4_:_
 for f being Function
for b2 being ordinal number holds
( ( ex a being ordinal number st a in dom f implies ( b2 = base- f iff f is b2 -based ) ) & ( ( for a being ordinal number holds not a in dom f ) implies ( b2 = base- f iff b2 = 0 ) ) );

:: deftheorem Def5 defines limit- EXCHSORT:def_5_:_
 for f being Function
for b2 being ordinal number holds
( ( ex a being ordinal number st a in dom f implies ( b2 = limit- f iff f is b2 -limited ) ) & ( ( for a being ordinal number holds not a in dom f ) implies ( b2 = limit- f iff b2 = 0 ) ) );

definition
let f be Function;
func len- f ->  ordinal number  equals :: EXCHSORT:def 6
(limit- f) -^ (base- f);
coherence
 (limit- f) -^ (base- f) is ordinal number ;
end;

:: deftheorem  defines len- EXCHSORT:def_6_:_
 for f being Function holds len- f = (limit- f) -^ (base- f);

theorem Th15: :: EXCHSORT:15
( base- {} = 0 & limit- {} = 0 & len- {} = 0 )
proof
 for a being ordinal number holds not a in dom {} ;
hence  ( base- {} = 0 & limit- {} = 0 ) by Def4, Def5; ::_thesis: len- {} = 0
hence  len- {} = 0 by ORDINAL3:56; ::_thesis: verum
end;

theorem Th16: :: EXCHSORT:16
for f being Function holds limit- f = sup (dom f)
proof
let f be Function; ::_thesis: limit- f = sup (dom f)
percases ( for a being ordinal number holds a nin dom f or ex a being ordinal number st a in dom f ) ;
supposeA1: for a being ordinal number holds a nin dom f ; ::_thesis: limit- f = sup (dom f)
 On (dom f) c= 0
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in On (dom f) or x in 0 )
assume  x in On (dom f) ; ::_thesis: x in 0
then  ( x in dom f & x is ordinal ) by ORDINAL1:def_9;
hence  x in 0 by A1; ::_thesis: verum
end;
then  sup (dom f) c= 0 by ORDINAL2:def_3;
then  sup (dom f) = 0 ;
hence  limit- f = sup (dom f) by A1, Def5; ::_thesis: verum
end;
supposeA2: ex a being ordinal number st a in dom f ; ::_thesis: limit- f = sup (dom f)
 f is sup (dom f) -limited by Def3;
hence  limit- f = sup (dom f) by A2, Def5; ::_thesis: verum
end;
end;
end;

theorem :: EXCHSORT:17
for f being Function holds f is limit- f -limited
proof
let f be Function; ::_thesis: f is limit- f -limited
 limit- f = sup (dom f) by Th16;
hence  f is limit- f -limited by Def3; ::_thesis: verum
end;

theorem Th18: :: EXCHSORT:18
for a being ordinal number
for A being empty set holds A is a -based
proof
let a be ordinal number ; ::_thesis: for A being empty set holds A is a -based
let A be empty set ; ::_thesis: A is a -based
let b be ordinal number ; :: according to EXCHSORT:def_2 ::_thesis: ( b in proj1 A implies ( a in proj1 A & a c= b ) )
thus  ( b in proj1 A implies ( a in proj1 A & a c= b ) ) ; ::_thesis: verum
end;

registration
let a be ordinal number ;
let X, Y be set ;
cluster empty T-Sequence-like Relation-like Y -defined X -valued Function-like finite segmental a -based 0 -based for set ;
existence
 ex b1 being T-Sequence st
( b1 is Y -defined & b1 is X -valued & b1 is a -based & b1 is segmental & b1 is finite & b1 is empty )
proof
take A = {} [:Y,X:]; ::_thesis: ( A is Y -defined & A is X -valued & A is a -based & A is segmental & A is finite & A is empty )
thus  ( A is Y -defined & A is X -valued & A is a -based & A is segmental & A is finite & A is empty ) by Th18; ::_thesis: verum
end;
end;

definition
mode array is segmental Function;
end;

registration
let A be array;
cluster proj1 A ->  ordinal-membered ;
coherence
 dom A is ordinal-membered
proof
consider a, b being ordinal number  such that
A1: dom A = a \ b by Def1;
take  a ; :: according to ORDINAL6:def_1 ::_thesis: dom A c= a
thus  dom A c= a by A1; ::_thesis: verum
end;
end;

theorem :: EXCHSORT:19
for f being array holds
( f is 0 -limited iff f is empty )
proof
let f be array; ::_thesis: ( f is 0 -limited iff f is empty )
thus  ( f is 0 -limited implies f is empty ) ::_thesis: ( f is empty implies f is 0 -limited )
proof
assume  sup (dom f) = 0 ; :: according to EXCHSORT:def_3 ::_thesis: f is empty
then  dom f c= 0 by ORDINAL6:3;
hence  f is empty ; ::_thesis: verum
end;
assume  f is empty ; ::_thesis: f is 0 -limited
hence  sup (dom f) = 0 by ORDINAL2:18; :: according to EXCHSORT:def_3 ::_thesis: verum
end;

registration
cluster Relation-like Function-like segmental 0 -based  ->  T-Sequence-like for set ;
coherence
 for b1 being array st b1 is 0 -based holds
b1 is T-Sequence-like
proof
let s be array; ::_thesis: ( s is 0 -based implies s is T-Sequence-like )
assume A1: for b being ordinal number st b in proj1 s holds
( 0 in proj1 s & 0 c= b ) ; :: according to EXCHSORT:def_2 ::_thesis: s is T-Sequence-like
consider c, a being ordinal number  such that
A2: dom s = c \ a by Def1;
set x = the Element of c \ a;
now__::_thesis:_(_c_\_a_<>_{}_implies_dom_s_=_c_)
assume A3: c \ a <> {} ; ::_thesis: dom s = c
then  the Element of c \ a in c by XBOOLE_0:def_5;
then  0 in dom s by A1, A2, A3;
then  0 nin a by A2, XBOOLE_0:def_5;
then  a c= 0 by ORDINAL6:4;
then  a = 0 ;
hence  dom s = c by A2; ::_thesis: verum
end;
hence  dom s is ordinal by A2; :: according to ORDINAL1:def_7 ::_thesis: verum
end;
end;

definition
let X be set ;
mode array of X is X -valued array;
end;

definition
let X be 1-sorted ;
mode array of X is array of the carrier of X;
end;

definition
let a be ordinal number ;
let X be set ;
mode array of a,X is a -defined array of X;
end;


theorem Th20: :: EXCHSORT:20
for f being Function holds base- f = inf (dom f)
proof
let f be Function; ::_thesis: base- f = inf (dom f)
set A = f;
set b = inf (dom f);
A1: f is inf (dom f) -based by Th12;
percases ( ex a being ordinal number st a in dom f or for a being ordinal number holds not a in dom f ) ;
suppose ex a being ordinal number st a in dom f ; ::_thesis: base- f = inf (dom f)
hence  base- f = inf (dom f) by A1, Def4; ::_thesis: verum
end;
supposeA2: for a being ordinal number holds not a in dom f ; ::_thesis: base- f = inf (dom f)
set x = the Element of On (dom f);
now__::_thesis:_not_On_(dom_f)_<>_{}
assume  On (dom f) <> {} ; ::_thesis: contradiction
then  the Element of On (dom f) in dom f by ORDINAL1:def_9;
hence  contradiction by A2; ::_thesis: verum
end;
then  inf (dom f) = 0 by SETFAM_1:def_1;
hence  base- f = inf (dom f) by A2, Def4; ::_thesis: verum
end;
end;
end;

theorem :: EXCHSORT:21
for f being Function holds f is base- f -based
proof
let f be Function; ::_thesis: f is base- f -based
 base- f = inf (dom f) by Th20;
hence  f is base- f -based by Th12; ::_thesis: verum
end;

theorem :: EXCHSORT:22
for A being array holds dom A = (limit- A) \ (base- A)
proof
let A be array; ::_thesis: dom A = (limit- A) \ (base- A)
consider a, b being ordinal number  such that
A1: dom A = a \ b by Def1;
A2: limit- A = sup (dom A) by Th16;
A3: base- A = inf (dom A) by Th20;
thus  dom A c= (limit- A) \ (base- A) :: according to XBOOLE_0:def_10 ::_thesis: (limit- A) \ (base- A) c= dom A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom A or x in (limit- A) \ (base- A) )
assume  x in dom A ; ::_thesis: x in (limit- A) \ (base- A)
then A4: ( base- A c= x & x in limit- A ) by A2, A3, ORDINAL2:14, ORDINAL2:19;
then  ( x in base- A implies x in x ) ;
hence  x in (limit- A) \ (base- A) by A4, XBOOLE_0:def_5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (limit- A) \ (base- A) or x in dom A )
assume A5: x in (limit- A) \ (base- A) ; ::_thesis: x in dom A
then reconsider x = x as Ordinal ;
 ex c being ordinal number st
( c in dom A & x c= c ) by A2, A5, ORDINAL2:21;
then  ( a = limit- A & b = base- A ) by A1, A2, A3, Th6;
hence  x in dom A by A1, A5; ::_thesis: verum
end;

theorem Th23: :: EXCHSORT:23
for a, b being ordinal number
for A being array st dom A = a \ b & not A is empty holds
( base- A = b & limit- A = a )
proof
let a, b be ordinal number ; ::_thesis: for A being array st dom A = a \ b & not A is empty holds
( base- A = b & limit- A = a )
let A be array; ::_thesis: ( dom A = a \ b & not A is empty implies ( base- A = b & limit- A = a ) )
assume A1: ( dom A = a \ b & not A is empty ) ; ::_thesis: ( base- A = b & limit- A = a )
set x = the Element of dom A;
 dom A <> {} by A1;
then A2: the Element of dom A in a \ b by A1;
 ( b c= the Element of dom A & the Element of dom A in a ) by A1, ORDINAL6:5;
then A3: ( b in a & b nin b ) by ORDINAL1:12;
then  b in a \ b by XBOOLE_0:def_5;
then A4: b in sup (dom A) by A1, ORDINAL2:19;
 A is b -based
proof
let c be ordinal number ; :: according to EXCHSORT:def_2 ::_thesis: ( c in proj1 A implies ( b in proj1 A & b c= c ) )
thus  ( c in proj1 A implies ( b in proj1 A & b c= c ) ) by A1, A3, ORDINAL6:5; ::_thesis: verum
end;
hence  base- A = b by Def4, A1, A2; ::_thesis: limit- A = a
A5: a c= sup (dom A)
proof
let x be Ordinal; :: according to ORDINAL1:def_5 ::_thesis: ( not x in a or x in sup (dom A) )
assume A6: x in a ; ::_thesis: x in sup (dom A)
percases ( x in b or x nin b ) ;
suppose x in b ; ::_thesis: x in sup (dom A)
hence  x in sup (dom A) by A4, ORDINAL1:10; ::_thesis: verum
end;
suppose x nin b ; ::_thesis: x in sup (dom A)
then  x in a \ b by A6, XBOOLE_0:def_5;
hence  x in sup (dom A) by A1, ORDINAL2:19; ::_thesis: verum
end;
end;
end;
 sup (dom A) c= sup a by A1, ORDINAL2:22;
then  sup (dom A) c= a by ORDINAL2:18;
then  a = sup (dom A) by A5, XBOOLE_0:def_10;
hence  limit- A = a by Th16; ::_thesis: verum
end;

theorem Th24: :: EXCHSORT:24
for f being T-Sequence holds
( base- f = 0 & limit- f = dom f & len- f = dom f )
proof
let f be T-Sequence; ::_thesis: ( base- f = 0 & limit- f = dom f & len- f = dom f )
percases ( f = {} or f <> {} ) ;
suppose f = {} ; ::_thesis: ( base- f = 0 & limit- f = dom f & len- f = dom f )
hence  ( base- f = 0 & limit- f = dom f & len- f = dom f ) by Th15; ::_thesis: verum
end;
supposeA1: f <> {} ; ::_thesis: ( base- f = 0 & limit- f = dom f & len- f = dom f )
 (dom f) \ 0 = dom f ;
hence  ( base- f = 0 & limit- f = dom f ) by A1, Th23; ::_thesis: len- f = dom f
hence  len- f = dom f by ORDINAL3:56; ::_thesis: verum
end;
end;
end;

registration
let a, b be ordinal number ;
let X be set ;
cluster Relation-like a -defined X -valued INT -valued Function-like complex-valued real-valued natural-valued finite segmental b -based for set ;
existence
 ex b1 being array of a,X st
( b1 is b -based & b1 is natural-valued & b1 is INT -valued & b1 is real-valued & b1 is complex-valued & b1 is finite )
proof
set A = the empty array of a,X;
take  the empty array of a,X ; ::_thesis: ( the empty array of a,X is b -based & the empty array of a,X is natural-valued & the empty array of a,X is INT -valued & the empty array of a,X is real-valued & the empty array of a,X is complex-valued & the empty array of a,X is finite )
thus  ( the empty array of a,X is b -based & the empty array of a,X is natural-valued & the empty array of a,X is INT -valued & the empty array of a,X is real-valued & the empty array of a,X is complex-valued & the empty array of a,X is finite ) by Th18; ::_thesis: verum
end;
end;

registration
let a be ordinal number ;
let x be set ;
cluster{[a,x]} ->  segmental ;
coherence
 {[a,x]} is segmental
proof
take  succ a ; :: according to EXCHSORT:def_1 ::_thesis: ex b being ordinal number st proj1 {[a,x]} = (succ a) \ b
take  a ; ::_thesis: proj1 {[a,x]} = (succ a) \ a
thus  dom {[a,x]} = {a} by FUNCT_5:12
.= (succ a) \ a by Th4 ; ::_thesis: verum
end;
end;

registration
let a be ordinal number ;
let x be Nat;
cluster{[a,x]} ->  natural-valued for array;
coherence
 for b1 being array st b1 = {[a,x]} holds
b1 is natural-valued
proof
let A be array; ::_thesis: ( A = {[a,x]} implies A is natural-valued )
assume  A = {[a,x]} ; ::_thesis: A is natural-valued
then  rng A = {x} by FUNCT_5:12;
then  rng A c= NAT by MEMBERED:6;
hence  A is natural-valued by VALUED_0:def_6; ::_thesis: verum
end;
end;

registration
let a be ordinal number ;
let x be real number ;
cluster{[a,x]} ->  real-valued for array;
coherence
 for b1 being array st b1 = {[a,x]} holds
b1 is real-valued
proof
let A be array; ::_thesis: ( A = {[a,x]} implies A is real-valued )
assume  A = {[a,x]} ; ::_thesis: A is real-valued
then  rng A = {x} by FUNCT_5:12;
then  rng A c= REAL by MEMBERED:3;
hence  A is real-valued by VALUED_0:def_3; ::_thesis: verum
end;
end;

registration
let a be ordinal number ;
let X be non empty set ;
let x be Element of X;
cluster{[a,x]} -> X -valued for array;
coherence
 for b1 being array st b1 = {[a,x]} holds
b1 is X -valued
proof
let A be array; ::_thesis: ( A = {[a,x]} implies A is X -valued )
assume  A = {[a,x]} ; ::_thesis: A is X -valued
then  rng A = {x} by FUNCT_5:12;
hence  rng A c= X by ZFMISC_1:31; :: according to RELAT_1:def_19 ::_thesis: verum
end;
end;

registration
let a be ordinal number ;
let x be set ;
cluster{[a,x]} -> a -based succ a -limited for array;
coherence
 for b1 being array st b1 = {[a,x]} holds
( b1 is a -based & b1 is succ a -limited )
proof
let s be array; ::_thesis: ( s = {[a,x]} implies ( s is a -based & s is succ a -limited ) )
assume A1: s = {[a,x]} ; ::_thesis: ( s is a -based & s is succ a -limited )
A2: dom s = {a} by A1, FUNCT_5:12;
thus  s is a -based ::_thesis: s is succ a -limited
proof
let b be ordinal number ; :: according to EXCHSORT:def_2 ::_thesis: ( b in proj1 s implies ( a in proj1 s & a c= b ) )
assume A3: b in proj1 s ; ::_thesis: ( a in proj1 s & a c= b )
thus  ( a in proj1 s & a c= b ) by A3, A2, TARSKI:def_1; ::_thesis: verum
end;
 sup (dom s) = succ a by A2, ORDINAL2:23;
hence  s is succ a -limited by Def3; ::_thesis: verum
end;
end;

registration
let b be ordinal number ;
cluster non empty Relation-like INT -valued Function-like complex-valued real-valued natural-valued finite segmental b -based for set ;
existence
 ex b1 being array st
( not b1 is empty & b1 is b -based & b1 is natural-valued & b1 is INT -valued & b1 is real-valued & b1 is complex-valued & b1 is finite )
proof
set x = the Nat;
reconsider A = {[b, the Nat]} as natural-valued array ;
take  A ; ::_thesis: ( not A is empty & A is b -based & A is natural-valued & A is INT -valued & A is real-valued & A is complex-valued & A is finite )
thus  ( not A is empty & A is b -based & A is natural-valued & A is INT -valued & A is real-valued & A is complex-valued & A is finite ) ; ::_thesis: verum
end;
let X be non empty set ;
cluster non empty Relation-like X -valued Function-like finite segmental b -based for set ;
existence
 ex b1 being array st
( not b1 is empty & b1 is b -based & b1 is finite & b1 is X -valued )
proof
set x = the Element of X;
reconsider A = {[b, the Element of X]} as array of X ;
take  A ; ::_thesis: ( not A is empty & A is b -based & A is finite & A is X -valued )
thus  ( not A is empty & A is b -based & A is finite & A is X -valued ) ; ::_thesis: verum
end;
end;

notation
let s be T-Sequence;
synonym s last for  last s;
end;

definition
let A be array;
func last A ->  set  equals :: EXCHSORT:def 7
A . (union (dom A));
coherence
 A . (union (dom A)) is set ;
end;

:: deftheorem  defines last EXCHSORT:def_7_:_
 for A being array holds last A = A . (union (dom A));

registration
let A be T-Sequence;
identifyA last  with  last A;
compatibility
 A last = last A ;
end;

begin

definition
let f be Function;
attrf is descending  means :Def8: :: EXCHSORT:def 8
 for a, b being ordinal number st a in dom f & b in dom f & a in b holds
f . b c< f . a;
end;

:: deftheorem Def8 defines descending EXCHSORT:def_8_:_
 for f being Function holds
( f is descending iff for a, b being ordinal number st a in dom f & b in dom f & a in b holds
f . b c< f . a );

theorem :: EXCHSORT:25
for f being finite array st ( for a being ordinal number st a in dom f & succ a in dom f holds
f . (succ a) c< f . a ) holds
f is descending
proof
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 A1: 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 A2: ( 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
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 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  succ e1 c= 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 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 A9: S9[ 0 ] by A1, A2;
A10: for k being Nat st S9[k] holds
S9[k + 1]
proof
let k be Nat; ::_thesis: ( S9[k] implies S9[k + 1] )
 k + 1 = succ k by NAT_1:38;
then A11: H1(k + 1) = succ H1(k) by ORDINAL2:28;
then A12: ( H1(k) in H1(k + 1) & a in succ a ) by ORDINAL1:6;
then A13: ( H1(k) c= H1(k + 1) & a c= succ a ) by ORDINAL1:def_2;
 succ a c= H1(k) by ORDINAL3:24;
then A14: a c= H1(k) by A12, ORDINAL1:def_2;
assume A15: ( S9[k] & H1(k + 1) in dom f ) ; ::_thesis: f . H1(k + 1) c< f . a
then  H1(k) in dom f by A2, A13, A14, Th9;
then  ( f . H1(k) c< f . a & f . H1(k + 1) c< f . H1(k) ) by A1, A11, A15;
hence  f . H1(k + 1) c< f . a by XBOOLE_1:56; ::_thesis: verum
end;
A16: for k being Nat holds S9[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
end;

theorem Th26: :: EXCHSORT:26
for f being array st len- f = omega & ( for a being ordinal number st a in dom f & succ a in dom f holds
f . (succ a) c< f . a ) holds
f is descending
proof
let f be array; ::_thesis: ( len- f = omega & ( 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 A1: len- f = omega ; ::_thesis: ( ex a being ordinal number 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 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 A3: ( 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
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  succ e1 c= 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]
proof
let k be Nat; ::_thesis: ( S9[k] implies S9[k + 1] )
 k + 1 = succ k by NAT_1:38;
then A13: H1(k + 1) = succ H1(k) by ORDINAL2:28;
then A14: ( H1(k) in H1(k + 1) & a in succ a ) by ORDINAL1:6;
then A15: ( H1(k) c= H1(k + 1) & a c= succ a ) by ORDINAL1:def_2;
 succ a c= H1(k) by ORDINAL3:24;
then A16: a c= H1(k) by A14, ORDINAL1:def_2;
assume A17: ( S9[k] & H1(k + 1) in dom f ) ; ::_thesis: f . H1(k + 1) c< f . a
then  H1(k) in dom f by A3, A15, A16, Th9;
then  ( f . H1(k) c< f . a & f . H1(k + 1) c< f . H1(k) ) by A2, A13, A17;
hence  f . H1(k + 1) c< f . a by XBOOLE_1:56; ::_thesis: verum
end;
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; ::_thesis: verum
end;

theorem Th27: :: EXCHSORT:27
for f being T-Sequence st f is descending & f . 0 is finite holds
f is finite
proof
let f be T-Sequence; ::_thesis: ( f is descending & f . 0 is finite implies f is finite )
assume A1: f is descending ; ::_thesis: ( not f . 0 is finite or f is finite )
assume A2: f . 0 is finite ; ::_thesis: f is finite
deffunc H1( set ) ->  set = card (f . $1);
consider g being T-Sequence such that
A3: ( dom g = dom f & ( for a being ordinal number st a in dom f holds
g . a = H1(a) ) ) from ORDINAL2:sch_2();
defpred S9[ set ] means f . $1 is finite ;
A4: S9[ {} ] by A2;
A5: for a being ordinal number st S9[a] holds
S9[ succ a]
proof
let a be ordinal number ; ::_thesis: ( S9[a] implies S9[ succ a] )
percases ( succ a nin dom f or succ a in dom f ) ;
suppose succ a nin dom f ; ::_thesis: ( S9[a] implies S9[ succ a] )
hence  ( S9[a] implies S9[ succ a] ) by FUNCT_1:def_2; ::_thesis: verum
end;
supposeA6: succ a in dom f ; ::_thesis: ( S9[a] implies S9[ succ a] )
A7: a in succ a by ORDINAL1:6;
then  a in dom f by A6, ORDINAL1:10;
then  f . (succ a) c< f . a by A1, A6, A7, Def8;
then  f . (succ a) c= f . a by XBOOLE_0:def_8;
hence  ( S9[a] implies S9[ succ a] ) ; ::_thesis: verum
end;
end;
end;
A8: for a being ordinal number st a <> {} & a is limit_ordinal & ( for b being ordinal number st b in a holds
S9[b] ) holds
S9[a]
proof
let a be ordinal number ; ::_thesis: ( a <> {} & a is limit_ordinal & ( for b being ordinal number st b in a holds
S9[b] ) implies S9[a] )
assume  a <> {} ; ::_thesis: ( not a is limit_ordinal or ex b being ordinal number st
( b in a & not S9[b] ) or S9[a] )
then A9: 0 in a by ORDINAL3:8;
percases ( a in dom f or a nin dom f ) ;
suppose a in dom f ; ::_thesis: ( not a is limit_ordinal or ex b being ordinal number st
( b in a & not S9[b] ) or S9[a] )
then  ( 0 in dom f & a in dom f ) by ORDINAL3:8;
then  f . a c< f . 0 by A1, A9, Def8;
then  f . a c= f . 0 by XBOOLE_0:def_8;
hence  ( not a is limit_ordinal or ex b being ordinal number st
( b in a & not S9[b] ) or S9[a] ) by A2; ::_thesis: verum
end;
suppose a nin dom f ; ::_thesis: ( not a is limit_ordinal or ex b being ordinal number st
( b in a & not S9[b] ) or S9[a] )
hence  ( not a is limit_ordinal or ex b being ordinal number st
( b in a & not S9[b] ) or S9[a] ) by FUNCT_1:def_2; ::_thesis: verum
end;
end;
end;
A10: for a being ordinal number holds S9[a] from ORDINAL2:sch_1(A4, A5, A8);
 g is decreasing
proof
let a be ordinal number ; :: according to ORDINAL5:def_1 ::_thesis: for b1 being set holds
( not a in b1 or not b1 in proj1 g or g . b1 in g . a )
let b be ordinal number ; ::_thesis: ( not a in b or not b in proj1 g or g . b in g . a )
assume A11: ( a in b & b in dom g ) ; ::_thesis: g . b in g . a
then  a in dom f by A3, ORDINAL1:10;
then  ( g . a = H1(a) & f . a is finite & f . b c< f . a & g . b = H1(b) & f . b is finite ) by A1, A3, A11, A10, Def8;
hence  g . b in g . a by CARD_2:48; ::_thesis: verum
end;
hence  f is finite by A3, FINSET_1:10; ::_thesis: verum
end;

theorem :: EXCHSORT:28
for f being T-Sequence st f is descending & f . 0 is finite & ( for a being ordinal number st f . a <> {} holds
succ a in dom f ) holds
last f = {}
proof
let f be T-Sequence; ::_thesis: ( f is descending & f . 0 is finite & ( for a being ordinal number st f . a <> {} holds
succ a in dom f ) implies last f = {} )
assume that
A1: ( f is descending & f . 0 is finite ) and
A2: for a being ordinal number st f . a <> {} holds
succ a in dom f ; ::_thesis: last f = {}
 f is finite by A1, Th27;
then reconsider d = dom f as finite Ordinal ;
set u = union d;
percases ( d = 0 or d <> 0 ) ;
suppose d = 0 ; ::_thesis: last f = {}
hence  last f = {} by FUNCT_1:def_2; ::_thesis: verum
end;
suppose d <> 0 ; ::_thesis: last f = {}
then consider n being Nat such that
A3: d = n + 1 by NAT_1:6;
A4: d = succ n by A3, NAT_1:38;
then A5: union d = n by ORDINAL2:2;
 ( f . (union d) <> 0 implies d in d ) by A2, A4, A5;
hence  last f = {} ; ::_thesis: verum
end;
end;
end;

scheme :: EXCHSORT:sch 1
A{ F1() ->  T-Sequence, F2( set ) ->  set } :
 F1() is finite
provided
A1: F2((F1() . 0)) is finite and
A2: for a being ordinal number st succ a in dom F1() & F2((F1() . a)) is finite holds
F2((F1() . (succ a))) c< F2((F1() . a))
proof
deffunc H1( set ) ->  set = F2((F1() . $1));
consider F being T-Sequence such that
A3: ( dom F = dom F1() & ( for a being ordinal number st a in dom F1() holds
F . a = H1(a) ) ) from ORDINAL2:sch_2();
percases ( dom F in omega or omega c= dom F ) by ORDINAL6:4;
suppose dom F in omega ; ::_thesis: F1() is finite
hence  F1() is finite by A3, FINSET_1:10; ::_thesis: verum
end;
supposeA4: omega c= dom F ; ::_thesis: F1() is finite
set f = F | omega;
A5: dom (F | omega) = omega by A4, RELAT_1:62;
A6: len- (F | omega) = dom (F | omega) by Th24;
A7: 0 in omega by ORDINAL1:def_11;
A8: (F | omega) . 0 = F . 0 by A7, A5, FUNCT_1:47
.= H1( 0 ) by A3, A7, A4 ;
defpred S9[ Nat] means (F | omega) . $1 is finite ;
A9: S9[ 0 ] by A1, A8;
A10: for n being Nat st S9[n] holds
S9[n + 1]
proof
let n be Nat; ::_thesis: ( S9[n] implies S9[n + 1] )
set a = n;
assume A11: S9[n] ; ::_thesis: S9[n + 1]
A12: ( n in omega & succ n in omega ) by ORDINAL1:def_12;
then A13: ( n in dom F & succ n in dom F & (F | omega) . n = F . n & (F | omega) . (succ n) = F . (succ n) ) by A4, A5, FUNCT_1:47;
 ( F . n = H1(n) & F . (succ n) = H1( succ n) ) by A3, A4, A12;
then  (F | omega) . (succ n) c< (F | omega) . n by A2, A3, A11, A13;
then  (F | omega) . (succ n) c= (F | omega) . n by XBOOLE_0:def_8;
hence  S9[n + 1] by A11, NAT_1:38; ::_thesis: verum
end;
A14: for n being Nat holds S9[n] from NAT_1:sch_2(A9, A10);
 for a being ordinal number st a in dom (F | omega) & succ a in dom (F | omega) holds
(F | omega) . (succ a) c< (F | omega) . a
proof
let a be ordinal number ; ::_thesis: ( a in dom (F | omega) & succ a in dom (F | omega) implies (F | omega) . (succ a) c< (F | omega) . a )
assume A15: ( a in dom (F | omega) & succ a in dom (F | omega) ) ; ::_thesis: (F | omega) . (succ a) c< (F | omega) . a
then reconsider n = a as Nat by A5;
A16: ( S9[n] & (F | omega) . a = F . a & (F | omega) . (succ a) = F . (succ a) ) by A15, A14, FUNCT_1:47;
 ( F . a = H1(a) & F . (succ a) = H1( succ a) ) by A3, A15, A4, A5;
hence  (F | omega) . (succ a) c< (F | omega) . a by A2, A3, A16, A15, A4, A5; ::_thesis: verum
end;
then  F | omega is descending by A6, Th26, A4, RELAT_1:62;
then  F | omega is finite by A1, A8, Th27;
hence  F1() is finite by A5; ::_thesis: verum
end;
end;
end;

begin

registration
let X be set ;
let f be X -defined Function;
let a, b be set ;
cluster Swap (f,a,b) -> X -defined ;
coherence
 Swap (f,a,b) is X -defined
proof
 dom (Swap (f,a,b)) = dom f by FUNCT_7:99;
hence  dom (Swap (f,a,b)) c= X ; :: according to RELAT_1:def_18 ::_thesis: verum
end;
end;

registration
let X be set ;
let f be X -valued Function;
let x, y be set ;
cluster Swap (f,x,y) -> X -valued ;
coherence
 Swap (f,x,y) is X -valued
proof
 rng (Swap (f,x,y)) = rng f by FUNCT_7:103;
hence  rng (Swap (f,x,y)) c= X by RELAT_1:def_19; :: according to RELAT_1:def_19 ::_thesis: verum
end;
end;

theorem Th29: :: EXCHSORT:29
for x, y being set
for f being Function st x in dom f & y in dom f holds
(Swap (f,x,y)) . x = f . y
proof
let x, y be set ; ::_thesis: for f being Function st x in dom f & y in dom f holds
(Swap (f,x,y)) . x = f . y
let f be Function; ::_thesis: ( x in dom f & y in dom f implies (Swap (f,x,y)) . x = f . y )
assume A1: ( x in dom f & y in dom f ) ; ::_thesis: (Swap (f,x,y)) . x = f . y
then A2: Swap (f,x,y) = (f +* (x,(f . y))) +* (y,(f . x)) by FUNCT_7:def_12;
A3: dom f = dom (f +* (x,(f . y))) by FUNCT_7:30;
now__::_thesis:_(_x_<>_y_implies_(Swap_(f,x,y))_._x_=_f_._y_)
assume  x <> y ; ::_thesis: (Swap (f,x,y)) . x = f . y
then  (Swap (f,x,y)) . x = (f +* (x,(f . y))) . x by A2, FUNCT_7:32;
hence  (Swap (f,x,y)) . x = f . y by A1, FUNCT_7:31; ::_thesis: verum
end;
hence  (Swap (f,x,y)) . x = f . y by A3, A1, A2, FUNCT_7:31; ::_thesis: verum
end;

theorem Th30: :: EXCHSORT:30
for X, x, y being set
for f being array of X st x in dom f & y in dom f holds
(Swap (f,x,y)) /. x = f /. y
proof
let X, x, y be set ; ::_thesis: for f being array of X st x in dom f & y in dom f holds
(Swap (f,x,y)) /. x = f /. y
let f be array of X; ::_thesis: ( x in dom f & y in dom f implies (Swap (f,x,y)) /. x = f /. y )
assume A1: ( x in dom f & y in dom f ) ; ::_thesis: (Swap (f,x,y)) /. x = f /. y
 dom (Swap (f,x,y)) = dom f by FUNCT_7:99;
hence (Swap (f,x,y)) /. x = (Swap (f,x,y)) . x by A1, PARTFUN1:def_6
.= f . y by A1, Th29
.= f /. y by A1, PARTFUN1:def_6 ;
::_thesis: verum
end;

theorem Th31: :: EXCHSORT:31
for x, y being set
for f being Function st x in dom f & y in dom f holds
(Swap (f,x,y)) . y = f . x
proof
let x, y be set ; ::_thesis: for f being Function st x in dom f & y in dom f holds
(Swap (f,x,y)) . y = f . x
let f be Function; ::_thesis: ( x in dom f & y in dom f implies (Swap (f,x,y)) . y = f . x )
assume A1: ( x in dom f & y in dom f ) ; ::_thesis: (Swap (f,x,y)) . y = f . x
then A2: Swap (f,x,y) = (f +* (x,(f . y))) +* (y,(f . x)) by FUNCT_7:def_12;
 dom f = dom (f +* (x,(f . y))) by FUNCT_7:30;
hence  (Swap (f,x,y)) . y = f . x by A1, A2, FUNCT_7:31; ::_thesis: verum
end;

theorem Th32: :: EXCHSORT:32
for X, x, y being set
for f being array of X st x in dom f & y in dom f holds
(Swap (f,x,y)) /. y = f /. x
proof
let X, x, y be set ; ::_thesis: for f being array of X st x in dom f & y in dom f holds
(Swap (f,x,y)) /. y = f /. x
let f be array of X; ::_thesis: ( x in dom f & y in dom f implies (Swap (f,x,y)) /. y = f /. x )
assume A1: ( x in dom f & y in dom f ) ; ::_thesis: (Swap (f,x,y)) /. y = f /. x
 dom (Swap (f,x,y)) = dom f by FUNCT_7:99;
hence (Swap (f,x,y)) /. y = (Swap (f,x,y)) . y by A1, PARTFUN1:def_6
.= f . x by A1, Th31
.= f /. x by A1, PARTFUN1:def_6 ;
::_thesis: verum
end;

theorem Th33: :: EXCHSORT:33
for z, x, y being set
for f being Function st z <> x & z <> y holds
(Swap (f,x,y)) . z = f . z
proof
let z, x, y be set ; ::_thesis: for f being Function st z <> x & z <> y holds
(Swap (f,x,y)) . z = f . z
let f be Function; ::_thesis: ( z <> x & z <> y implies (Swap (f,x,y)) . z = f . z )
assume A1: ( z <> x & z <> y ) ; ::_thesis: (Swap (f,x,y)) . z = f . z
percases ( ( x in dom f & y in dom f ) or not x in dom f or not y in dom f ) ;
suppose ( x in dom f & y in dom f ) ; ::_thesis: (Swap (f,x,y)) . z = f . z
then  Swap (f,x,y) = (f +* (x,(f . y))) +* (y,(f . x)) by FUNCT_7:def_12;
hence (Swap (f,x,y)) . z = (f +* (x,(f . y))) . z by A1, FUNCT_7:32
.= f . z by A1, FUNCT_7:32 ;
::_thesis: verum
end;
suppose ( not x in dom f or not y in dom f ) ; ::_thesis: (Swap (f,x,y)) . z = f . z
hence  (Swap (f,x,y)) . z = f . z by FUNCT_7:def_12; ::_thesis: verum
end;
end;
end;

theorem Th34: :: EXCHSORT:34
for X, z, x, y being set
for f being array of X st z in dom f & z <> x & z <> y holds
(Swap (f,x,y)) /. z = f /. z
proof
let X, z, x, y be set ; ::_thesis: for f being array of X st z in dom f & z <> x & z <> y holds
(Swap (f,x,y)) /. z = f /. z
let f be array of X; ::_thesis: ( z in dom f & z <> x & z <> y implies (Swap (f,x,y)) /. z = f /. z )
assume A1: ( z in dom f & z <> x & z <> y ) ; ::_thesis: (Swap (f,x,y)) /. z = f /. z
 dom (Swap (f,x,y)) = dom f by FUNCT_7:99;
hence (Swap (f,x,y)) /. z = (Swap (f,x,y)) . z by A1, PARTFUN1:def_6
.= f . z by A1, Th33
.= f /. z by A1, PARTFUN1:def_6 ;
::_thesis: verum
end;

theorem :: EXCHSORT:35
for x, y being set
for f being Function st x in dom f & y in dom f holds
Swap (f,x,y) = Swap (f,y,x)
proof
let x, y be set ; ::_thesis: for f being Function st x in dom f & y in dom f holds
Swap (f,x,y) = Swap (f,y,x)
let f be Function; ::_thesis: ( x in dom f & y in dom f implies Swap (f,x,y) = Swap (f,y,x) )
assume A1: ( x in dom f & y in dom f ) ; ::_thesis: Swap (f,x,y) = Swap (f,y,x)
A2: ( dom (Swap (f,x,y)) = dom f & dom (Swap (f,y,x)) = dom f ) by FUNCT_7:99;
now__::_thesis:_for_z_being_set_st_z_in_dom_f_holds_
(Swap_(f,x,y))_._z_=_(Swap_(f,y,x))_._z
let z be set ; ::_thesis: ( z in dom f implies (Swap (f,x,y)) . b1 = (Swap (f,y,x)) . b1 )
assume  z in dom f ; ::_thesis: (Swap (f,x,y)) . b1 = (Swap (f,y,x)) . b1
percases ( ( z = x & z = y ) or ( z = x & z <> y ) or ( z <> x & z = y ) or ( z <> x & z <> y ) ) ;
suppose ( z = x & z = y ) ; ::_thesis: (Swap (f,x,y)) . b1 = (Swap (f,y,x)) . b1
hence  (Swap (f,x,y)) . z = (Swap (f,y,x)) . z ; ::_thesis: verum
end;
suppose ( z = x & z <> y ) ; ::_thesis: (Swap (f,x,y)) . b1 = (Swap (f,y,x)) . b1
then  ( (Swap (f,x,y)) . z = f . y & (Swap (f,y,x)) . z = f . y ) by A1, Th29, Th31;
hence  (Swap (f,x,y)) . z = (Swap (f,y,x)) . z ; ::_thesis: verum
end;
suppose ( z <> x & z = y ) ; ::_thesis: (Swap (f,x,y)) . b1 = (Swap (f,y,x)) . b1
then  ( (Swap (f,x,y)) . z = f . x & (Swap (f,y,x)) . z = f . x ) by A1, Th29, Th31;
hence  (Swap (f,x,y)) . z = (Swap (f,y,x)) . z ; ::_thesis: verum
end;
suppose ( z <> x & z <> y ) ; ::_thesis: (Swap (f,x,y)) . b1 = (Swap (f,y,x)) . b1
then  ( (Swap (f,x,y)) . z = f . z & (Swap (f,y,x)) . z = f . z ) by Th33;
hence  (Swap (f,x,y)) . z = (Swap (f,y,x)) . z ; ::_thesis: verum
end;
end;
end;
hence  Swap (f,x,y) = Swap (f,y,x) by A2, FUNCT_1:2; ::_thesis: verum
end;

registration
let X be non empty set ;
cluster non empty Relation-like X -valued Function-like onto for set ;
existence
 ex b1 being non empty X -valued Function st b1 is onto
proof
take  id X ; ::_thesis: id X is onto
thus  id X is onto ; ::_thesis: verum
end;
end;

registration
let X be non empty set ;
let f be non empty X -valued onto Function;
let x, y be Element of dom f;
cluster Swap (f,x,y) ->  onto ;
coherence
 Swap (f,x,y) is onto
proof
 rng (Swap (f,x,y)) = rng f by FUNCT_7:103;
hence  rng (Swap (f,x,y)) = X by FUNCT_2:def_3; :: according to FUNCT_2:def_3 ::_thesis: verum
end;
end;

registration
let A be array;
let x, y be set ;
cluster Swap (A,x,y) ->  segmental ;
coherence
 Swap (A,x,y) is segmental
proof
consider a1, a2 being ordinal number  such that
A1: dom A = a1 \ a2 by Def1;
take  a1 ; :: according to EXCHSORT:def_1 ::_thesis: ex b being ordinal number st proj1 (Swap (A,x,y)) = a1 \ b
take  a2 ; ::_thesis: proj1 (Swap (A,x,y)) = a1 \ a2
thus  proj1 (Swap (A,x,y)) = a1 \ a2 by A1, FUNCT_7:99; ::_thesis: verum
end;
end;

theorem :: EXCHSORT:36
for x, y being set
for A being array st x in dom A & y in dom A holds
Swap ((Swap (A,x,y)),x,y) = A
proof
let x, y be set ; ::_thesis: for A being array st x in dom A & y in dom A holds
Swap ((Swap (A,x,y)),x,y) = A
let A be array; ::_thesis: ( x in dom A & y in dom A implies Swap ((Swap (A,x,y)),x,y) = A )
assume A1: ( x in dom A & y in dom A ) ; ::_thesis: Swap ((Swap (A,x,y)),x,y) = A
set B = Swap (A,x,y);
set C = Swap ((Swap (A,x,y)),x,y);
A2: ( dom (Swap ((Swap (A,x,y)),x,y)) = dom (Swap (A,x,y)) & dom (Swap (A,x,y)) = dom A ) by FUNCT_7:99;
now__::_thesis:_for_z_being_set_st_z_in_dom_(Swap_(A,x,y))_holds_
(Swap_((Swap_(A,x,y)),x,y))_._z_=_A_._z
let z be set ; ::_thesis: ( z in dom (Swap (A,x,y)) implies (Swap ((Swap (A,x,y)),x,y)) . b1 = A . b1 )
assume  z in dom (Swap (A,x,y)) ; ::_thesis: (Swap ((Swap (A,x,y)),x,y)) . b1 = A . b1
percases ( ( z <> x & z <> y ) or z = x or z = y ) ;
supposeA3: ( z <> x & z <> y ) ; ::_thesis: (Swap ((Swap (A,x,y)),x,y)) . b1 = A . b1
hence (Swap ((Swap (A,x,y)),x,y)) . z = (Swap (A,x,y)) . z by Th33
.= A . z by A3, Th33 ;
::_thesis: verum
end;
supposeA4: z = x ; ::_thesis: (Swap ((Swap (A,x,y)),x,y)) . b1 = A . b1
hence (Swap ((Swap (A,x,y)),x,y)) . z = (Swap (A,x,y)) . y by A1, A2, Th29
.= A . z by A1, A4, Th31 ;
::_thesis: verum
end;
supposeA5: z = y ; ::_thesis: (Swap ((Swap (A,x,y)),x,y)) . b1 = A . b1
hence (Swap ((Swap (A,x,y)),x,y)) . z = (Swap (A,x,y)) . x by A1, A2, Th31
.= A . z by A1, A5, Th29 ;
::_thesis: verum
end;
end;
end;
hence  Swap ((Swap (A,x,y)),x,y) = A by A2, FUNCT_1:2; ::_thesis: verum
end;

registration
let A be real-valued array;
let x, y be set ;
cluster Swap (A,x,y) ->  real-valued for array;
coherence
 for b1 being array st b1 = Swap (A,x,y) holds
b1 is real-valued
proof
let B be array; ::_thesis: ( B = Swap (A,x,y) implies B is real-valued )
assume A1: B = Swap (A,x,y) ; ::_thesis: B is real-valued
let z be set ; :: according to VALUED_0:def_9 ::_thesis: ( not z in proj1 B or B . z is real )
assume  z in dom B ; ::_thesis: B . z is real
then A2: ( z in dom A & ( x = z or x <> z ) & ( y = z or y <> z ) ) by A1, FUNCT_7:99;
 ( ( not x in dom A or not y in dom A ) implies B = A ) by A1, FUNCT_7:def_12;
then  ( B . z = A . y or B . z = A . x or B . z = A . z ) by A1, A2, Th29, Th31, Th33;
hence  B . z is real ; ::_thesis: verum
end;
end;

begin

definition
let A be array;
mode permutation of A ->  array means :Def9: :: EXCHSORT:def 9
 ex f being Permutation of (dom A) st it = A * f;
existence
 ex b1 being array ex f being Permutation of (dom A) st b1 = A * f
proof
take  A ; ::_thesis: ex f being Permutation of (dom A) st A = A * f
take  id (dom A) ; ::_thesis: A = A * (id (dom A))
thus  A = A * (id (dom A)) by RELAT_1:51; ::_thesis: verum
end;
end;

:: deftheorem Def9 defines permutation EXCHSORT:def_9_:_
 for A, b2 being array holds
( b2 is permutation of A iff ex f being Permutation of (dom A) st b2 = A * f );

theorem Th37: :: EXCHSORT:37
for A being array
for B being permutation of A holds
( dom B = dom A & rng B = rng A )
proof
let A be array; ::_thesis: for B being permutation of A holds
( dom B = dom A & rng B = rng A )
let B be permutation of A; ::_thesis: ( dom B = dom A & rng B = rng A )
consider f being Permutation of (dom A) such that
A1: B = A * f by Def9;
 ( dom A <> {} implies dom A <> {} ) ;
then  ( rng f = dom A & dom f = dom A ) by FUNCT_2:def_1, FUNCT_2:def_3;
hence  ( dom B = dom A & rng B = rng A ) by A1, RELAT_1:27, RELAT_1:28; ::_thesis: verum
end;

theorem Th38: :: EXCHSORT:38
for A being array holds A is permutation of A
proof
let A be array; ::_thesis: A is permutation of A
take  id (dom A) ; :: according to EXCHSORT:def_9 ::_thesis: A = A * (id (dom A))
thus  A = A * (id (dom A)) by RELAT_1:51; ::_thesis: verum
end;

theorem Th39: :: EXCHSORT:39
for A, B being array st A is permutation of B holds
B is permutation of A
proof
let A, B be array; ::_thesis: ( A is permutation of B implies B is permutation of A )
assume A1: A is permutation of B ; ::_thesis: B is permutation of A
then A2: dom A = dom B by Th37;
consider f being Permutation of (dom B) such that
A3: A = B * f by A1, Def9;
reconsider g = f " as Permutation of (dom A) by A2;
take  g ; :: according to EXCHSORT:def_9 ::_thesis: B = A * g
thus B = B * (id (dom B)) by RELAT_1:52
.= B * (f * g) by FUNCT_2:61
.= A * g by A3, RELAT_1:36 ; ::_thesis: verum
end;

theorem Th40: :: EXCHSORT:40
for A, B, C being array st A is permutation of B & B is permutation of C holds
A is permutation of C
proof
let A, B, C be array; ::_thesis: ( A is permutation of B & B is permutation of C implies A is permutation of C )
assume A1: ( A is permutation of B & B is permutation of C ) ; ::_thesis: A is permutation of C
then A2: dom C = dom B by Th37;
consider f being Permutation of (dom B) such that
A3: A = B * f by A1, Def9;
consider g being Permutation of (dom C) such that
A4: B = C * g by A1, Def9;
reconsider h = g * f as Permutation of (dom C) by A2;
take  h ; :: according to EXCHSORT:def_9 ::_thesis: A = C * h
thus  A = C * h by A3, A4, RELAT_1:36; ::_thesis: verum
end;

theorem Th41: :: EXCHSORT:41
for X, x, y being set holds Swap ((id X),x,y) is one-to-one
proof
let X, x, y be set ; ::_thesis: Swap ((id X),x,y) is one-to-one
A1: dom (id X) = X ;
percases ( ( x in X & y in X ) or not x in X or not y in X ) ;
supposeA2: ( x in X & y in X ) ; ::_thesis: Swap ((id X),x,y) is one-to-one
set g = id X;
set f = Swap ((id X),x,y);
let z be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not z in proj1 (Swap ((id X),x,y)) or not b1 in proj1 (Swap ((id X),x,y)) or not (Swap ((id X),x,y)) . z = (Swap ((id X),x,y)) . b1 or z = b1 )
let t be set ; ::_thesis: ( not z in proj1 (Swap ((id X),x,y)) or not t in proj1 (Swap ((id X),x,y)) or not (Swap ((id X),x,y)) . z = (Swap ((id X),x,y)) . t or z = t )
assume A3: ( z in dom (Swap ((id X),x,y)) & t in dom (Swap ((id X),x,y)) & (Swap ((id X),x,y)) . z = (Swap ((id X),x,y)) . t ) ; ::_thesis: z = t
A4: ( (id X) . z = z & (id X) . t = t & (id X) . x = x & (id X) . y = y ) by A2, A3, FUNCT_1:17;
then A5: ( ( z = x implies (Swap ((id X),x,y)) . z = y ) & ( z = y implies (Swap ((id X),x,y)) . z = x ) & ( z <> x & z <> y implies (Swap ((id X),x,y)) . z = z ) ) by A2, A1, Th29, Th31, Th33;
 ( ( t = x implies (Swap ((id X),x,y)) . t = y ) & ( t = y implies (Swap ((id X),x,y)) . t = x ) & ( t <> x & t <> y implies (Swap ((id X),x,y)) . t = t ) ) by A2, A1, A4, Th29, Th31, Th33;
hence  z = t by A3, A5; ::_thesis: verum
end;
suppose ( not x in X or not y in X ) ; ::_thesis: Swap ((id X),x,y) is one-to-one
hence  Swap ((id X),x,y) is one-to-one by A1, FUNCT_7:def_12; ::_thesis: verum
end;
end;
end;

registration
let X be non empty set ;
let x, y be Element of X;
cluster Swap ((id X),x,y) -> X -defined X -valued one-to-one ;
coherence
 ( Swap ((id X),x,y) is one-to-one & Swap ((id X),x,y) is X -valued & Swap ((id X),x,y) is X -defined ) by Th41;
end;

registration
let X be non empty set ;
let x, y be Element of X;
cluster Swap ((id X),x,y) ->  total onto ;
coherence
 ( Swap ((id X),x,y) is onto & Swap ((id X),x,y) is total )
proof
A1: dom (id X) = X ;
reconsider a = x, b = y as Element of dom (id X) ;
 Swap ((id X),a,b) is onto ;
hence  Swap ((id X),x,y) is onto ; ::_thesis: Swap ((id X),x,y) is total
thus  dom (Swap ((id X),x,y)) = X by A1, FUNCT_7:99; :: according to PARTFUN1:def_2 ::_thesis: verum
end;
end;

definition
let X, Y be non empty set ;
let f be Function of X,Y;
let x, y be Element of X;
:: original: Swap
redefine func Swap (f,x,y) ->  Function of X,Y;
coherence
 Swap (f,x,y) is Function of X,Y
proof
set g = Swap (f,x,y);
A1: dom f = X by FUNCT_2:def_1;
A2: ( dom (Swap (f,x,y)) = dom f & rng (Swap (f,x,y)) = rng f ) by FUNCT_7:99, FUNCT_7:103;
 rng f c= Y by RELAT_1:def_19;
hence  Swap (f,x,y) is Function of X,Y by A1, A2, FUNCT_2:2; ::_thesis: verum
end;
end;

theorem Th42: :: EXCHSORT:42
for x, X, y being set
for f being Function
for A being array st x in X & y in X & f = Swap ((id X),x,y) & X = dom A holds
Swap (A,x,y) = A * f
proof
let x, X, y be set ; ::_thesis: for f being Function
for A being array st x in X & y in X & f = Swap ((id X),x,y) & X = dom A holds
Swap (A,x,y) = A * f
let f be Function; ::_thesis: for A being array st x in X & y in X & f = Swap ((id X),x,y) & X = dom A holds
Swap (A,x,y) = A * f
let A be array; ::_thesis: ( x in X & y in X & f = Swap ((id X),x,y) & X = dom A implies Swap (A,x,y) = A * f )
assume that
A1: ( x in X & y in X ) and
A2: ( f = Swap ((id X),x,y) & X = dom A ) ; ::_thesis: Swap (A,x,y) = A * f
set g = id X;
set s = Swap (A,x,y);
A3: ( dom (id X) = X & rng (id X) = X ) ;
then A4: ( dom f = X & rng f = X ) by A2, FUNCT_7:99, FUNCT_7:103;
A5: dom (Swap (A,x,y)) = dom A by FUNCT_7:99;
A6: dom (A * f) = dom f by A2, A4, RELAT_1:27;
now__::_thesis:_for_z_being_set_st_z_in_X_holds_
(Swap_(A,x,y))_._z_=_(A_*_f)_._z
let z be set ; ::_thesis: ( z in X implies (Swap (A,x,y)) . z = (A * f) . z )
assume A7: z in X ; ::_thesis: (Swap (A,x,y)) . z = (A * f) . z
A8: ( (id X) . x = x & (id X) . y = y & (id X) . z = z ) by A1, A7, FUNCT_1:17;
 ( z = x or z = y or ( z <> x & z <> y ) ) ;
then  ( ( (Swap (A,x,y)) . z = A . y & f . z = (id X) . y ) or ( (Swap (A,x,y)) . z = A . x & f . z = (id X) . x ) or ( (Swap (A,x,y)) . z = A . z & f . z = (id X) . z ) ) by A1, A2, A3, Th29, Th31, Th33;
hence  (Swap (A,x,y)) . z = (A * f) . z by A7, A8, A4, FUNCT_1:13; ::_thesis: verum
end;
hence  Swap (A,x,y) = A * f by A2, A4, A5, A6, FUNCT_1:2; ::_thesis: verum
end;

theorem Th43: :: EXCHSORT:43
for x, y being set
for A being array st x in dom A & y in dom A holds
( Swap (A,x,y) is permutation of A & A is permutation of Swap (A,x,y) )
proof
let x, y be set ; ::_thesis: for A being array st x in dom A & y in dom A holds
( Swap (A,x,y) is permutation of A & A is permutation of Swap (A,x,y) )
let A be array; ::_thesis: ( x in dom A & y in dom A implies ( Swap (A,x,y) is permutation of A & A is permutation of Swap (A,x,y) ) )
set X = dom A;
assume A1: ( x in dom A & y in dom A ) ; ::_thesis: ( Swap (A,x,y) is permutation of A & A is permutation of Swap (A,x,y) )
thus  Swap (A,x,y) is permutation of A ::_thesis: A is permutation of Swap (A,x,y)
proof
reconsider X = dom A as non empty set by A1;
reconsider x = x, y = y as Element of X by A1;
reconsider f = Swap ((id X),x,y) as Permutation of (dom A) ;
take  f ; :: according to EXCHSORT:def_9 ::_thesis: Swap (A,x,y) = A * f
thus  Swap (A,x,y) = A * f by Th42; ::_thesis: verum
end;
hence  A is permutation of Swap (A,x,y) by Th39; ::_thesis: verum
end;

theorem :: EXCHSORT:44
for x, y being set
for A, B being array st x in dom A & y in dom A & A is permutation of B holds
( Swap (A,x,y) is permutation of B & A is permutation of Swap (B,x,y) )
proof
let x, y be set ; ::_thesis: for A, B being array st x in dom A & y in dom A & A is permutation of B holds
( Swap (A,x,y) is permutation of B & A is permutation of Swap (B,x,y) )
let A, B be array; ::_thesis: ( x in dom A & y in dom A & A is permutation of B implies ( Swap (A,x,y) is permutation of B & A is permutation of Swap (B,x,y) ) )
set X = dom A;
assume A1: ( x in dom A & y in dom A & A is permutation of B ) ; ::_thesis: ( Swap (A,x,y) is permutation of B & A is permutation of Swap (B,x,y) )
then  dom A = dom B by Th37;
then  ( Swap (A,x,y) is permutation of A & B is permutation of Swap (B,x,y) ) by A1, Th43;
hence  ( Swap (A,x,y) is permutation of B & A is permutation of Swap (B,x,y) ) by A1, Th40; ::_thesis: verum
end;

begin

definition
let O be RelStr ;
let A be array of O;
attrA is ascending  means :: EXCHSORT:def 10
 for a, b being ordinal number st a in dom A & b in dom A & a in b holds
A /. a <= A /. b;
func inversions A ->  set  equals :: EXCHSORT:def 11
 {  [a,b] where a, b is Element of dom A : ( a in b & not A /. a <= A /. b )  }  ;
coherence
  {  [a,b] where a, b is Element of dom A : ( a in b & not A /. a <= A /. b )  }  is set ;
end;

:: deftheorem  defines ascending EXCHSORT:def_10_:_
 for O being RelStr
for A being array of O holds
( A is ascending iff for a, b being ordinal number st a in dom A & b in dom A & a in b holds
A /. a <= A /. b );

:: deftheorem  defines inversions EXCHSORT:def_11_:_
 for O being RelStr
for A being array of O holds inversions A =  {  [a,b] where a, b is Element of dom A : ( a in b & not A /. a <= A /. b )  }  ;

registration
let O be RelStr ;
cluster empty Relation-like the carrier of O -valued Function-like segmental  ->  empty ascending for set ;
coherence
 for b1 being empty array of O holds b1 is ascending
proof
let R be empty array of O; ::_thesis: R is ascending
let a be ordinal number ; :: according to EXCHSORT:def_10 ::_thesis: for b being ordinal number st a in dom R & b in dom R & a in b holds
R /. a <= R /. b
thus  for b being ordinal number st a in dom R & b in dom R & a in b holds
R /. a <= R /. b ; ::_thesis: verum
end;
let A be empty array of O;
cluster inversions A ->  empty ;
coherence
 inversions A is empty
proof
set w = the Element of inversions A;
assume  not inversions A is empty ; ::_thesis: contradiction
then  the Element of inversions A in inversions A ;
then consider a, b being Element of dom A such that
A1: ( the Element of inversions A = [a,b] & a in b & not A /. a <= A /. b ) ;
thus  contradiction by A1, SUBSET_1:def_1; ::_thesis: verum
end;
end;


theorem Th45: :: EXCHSORT:45
for O being non empty connected Poset
for x, y being Element of O holds
( x > y iff not x <= y )
proof
let O be non empty connected Poset; ::_thesis: for x, y being Element of O holds
( x > y iff not x <= y )
let x, y be Element of O; ::_thesis: ( x > y iff not x <= y )
A1: ( x <= y & y <= x implies x = y ) by YELLOW_0:def_3;
 ( ( x <= y or x >= y ) & x <= x ) by WAYBEL_0:def_29;
hence  ( x > y iff not x <= y ) by A1, ORDERS_2:def_6; ::_thesis: verum
end;

definition
let O be non empty connected Poset;
let R be array of O;
redefine func inversions R equals :: EXCHSORT:def 12
 {  [a,b] where a, b is Element of dom R : ( a in b & R /. a > R /. b )  }  ;
compatibility
 for b1 being set holds
( b1 = inversions R iff b1 =  {  [a,b] where a, b is Element of dom R : ( a in b & R /. a > R /. b )  }  )
proof
set N =  {  [a,b] where a, b is Element of dom R : ( a in b & R /. a > R /. b )  }  ;
 inversions R =  {  [a,b] where a, b is Element of dom R : ( a in b & R /. a > R /. b )  }
proof
thus  inversions R c=  {  [a,b] where a, b is Element of dom R : ( a in b & R /. a > R /. b )  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  [a,b] where a, b is Element of dom R : ( a in b & R /. a > R /. b )  }  c= inversions R
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in inversions R or x in  {  [a,b] where a, b is Element of dom R : ( a in b & R /. a > R /. b )  }  )
assume  x in inversions R ; ::_thesis: x in  {  [a,b] where a, b is Element of dom R : ( a in b & R /. a > R /. b )  }
then consider a, b being Element of dom R such that
A1: ( x = [a,b] & a in b & not R /. a <= R /. b ) ;
 R /. a > R /. b by A1, Th45;
hence  x in  {  [a,b] where a, b is Element of dom R : ( a in b & R /. a > R /. b )  }  by A1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  [a,b] where a, b is Element of dom R : ( a in b & R /. a > R /. b )  }  or x in inversions R )
assume  x in  {  [a,b] where a, b is Element of dom R : ( a in b & R /. a > R /. b )  }  ; ::_thesis: x in inversions R
then consider a, b being Element of dom R such that
A2: ( x = [a,b] & a in b & R /. a > R /. b ) ;
 not R /. a <= R /. b by A2, Th45;
hence  x in inversions R by A2; ::_thesis: verum
end;
hence  for b1 being set holds
( b1 = inversions R iff b1 =  {  [a,b] where a, b is Element of dom R : ( a in b & R /. a > R /. b )  }  ) ; ::_thesis: verum
end;
end;

:: deftheorem  defines inversions EXCHSORT:def_12_:_
 for O being non empty connected Poset
for R being array of O holds inversions R =  {  [a,b] where a, b is Element of dom R : ( a in b & R /. a > R /. b )  }  ;

theorem Th46: :: EXCHSORT:46
for x, y being set
for O being non empty connected Poset
for R being array of O holds
( [x,y] in inversions R iff ( x in dom R & y in dom R & x in y & R /. x > R /. y ) )
proof
let x, y be set ; ::_thesis: for O being non empty connected Poset
for R being array of O holds
( [x,y] in inversions R iff ( x in dom R & y in dom R & x in y & R /. x > R /. y ) )
let O be non empty connected Poset; ::_thesis: for R being array of O holds
( [x,y] in inversions R iff ( x in dom R & y in dom R & x in y & R /. x > R /. y ) )
let R be array of O; ::_thesis: ( [x,y] in inversions R iff ( x in dom R & y in dom R & x in y & R /. x > R /. y ) )
hereby  ::_thesis: ( x in dom R & y in dom R & x in y & R /. x > R /. y implies [x,y] in inversions R )
assume A1: [x,y] in inversions R ; ::_thesis: ( x in dom R & y in dom R & x in y & R /. x > R /. y )
then reconsider R1 = R as non empty Function ;
consider a, b being Element of dom R1 such that
A2: ( [x,y] = [a,b] & a in b & not R /. a <= R /. b ) by A1;
 ( x = a & y = b ) by A2, XTUPLE_0:1;
hence  ( x in dom R & y in dom R & x in y & R /. x > R /. y ) by A2, Th45; ::_thesis: verum
end;
thus  ( x in dom R & y in dom R & x in y & R /. x > R /. y implies [x,y] in inversions R ) ; ::_thesis: verum
end;

theorem Th47: :: EXCHSORT:47
for O being non empty connected Poset
for R being array of O holds inversions R c= [:(dom R),(dom R):]
proof
let O be non empty connected Poset; ::_thesis: for R being array of O holds inversions R c= [:(dom R),(dom R):]
let R be array of O; ::_thesis: inversions R c= [:(dom R),(dom R):]
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in inversions R or x in [:(dom R),(dom R):] )
assume A1: x in inversions R ; ::_thesis: x in [:(dom R),(dom R):]
then consider a, b being Element of dom R such that
A2: ( x = [a,b] & a in b & R /. a > R /. b ) ;
 ( a in dom R & b in dom R ) by A2, A1, Th46;
hence  x in [:(dom R),(dom R):] by A2, ZFMISC_1:def_2; ::_thesis: verum
end;

registration
let O be non empty connected Poset;
let R be finite array of O;
cluster inversions R ->  finite ;
coherence
 inversions R is finite
proof
 inversions R c= [:(dom R),(dom R):] by Th47;
hence  inversions R is finite ; ::_thesis: verum
end;
end;

theorem Th48: :: EXCHSORT:48
for O being non empty connected Poset
for R being array of O holds
( R is ascending iff inversions R = {} )
proof
let O be non empty connected Poset; ::_thesis: for R being array of O holds
( R is ascending iff inversions R = {} )
let R be array of O; ::_thesis: ( R is ascending iff inversions R = {} )
thus  ( R is ascending implies inversions R = {} ) ::_thesis: ( inversions R = {} implies R is ascending )
proof
assume A1: for a, b being ordinal number st a in dom R & b in dom R & a in b holds
R /. a <= R /. b ; :: according to EXCHSORT:def_10 ::_thesis: inversions R = {}
set x = the Element of inversions R;
assume A2: inversions R <> {} ; ::_thesis: contradiction
then  the Element of inversions R in inversions R ;
then consider a, b being Element of dom R such that
A3: ( the Element of inversions R = [a,b] & a in b & R /. a > R /. b ) ;
 R <> {} by A2;
then  R /. a <= R /. b by A1, A3;
hence  contradiction by A3, Th45; ::_thesis: verum
end;
assume A4: inversions R = {} ; ::_thesis: R is ascending
let a be ordinal number ; :: according to EXCHSORT:def_10 ::_thesis: for b being ordinal number st a in dom R & b in dom R & a in b holds
R /. a <= R /. b
let b be ordinal number ; ::_thesis: ( a in dom R & b in dom R & a in b implies R /. a <= R /. b )
assume  ( a in dom R & b in dom R & a in b ) ; ::_thesis: R /. a <= R /. b
then  ( R /. a > R /. b implies [a,b] in inversions R ) ;
hence  R /. a <= R /. b by A4, Th45; ::_thesis: verum
end;

theorem Th49: :: EXCHSORT:49
for x, y being set
for O being non empty connected Poset
for R being array of O st [x,y] in inversions R holds
[y,x] nin inversions R
proof
let x, y be set ; ::_thesis: for O being non empty connected Poset
for R being array of O st [x,y] in inversions R holds
[y,x] nin inversions R
let O be non empty connected Poset; ::_thesis: for R being array of O st [x,y] in inversions R holds
[y,x] nin inversions R
let R be array of O; ::_thesis: ( [x,y] in inversions R implies [y,x] nin inversions R )
assume  [x,y] in inversions R ; ::_thesis: [y,x] nin inversions R
then  y nin x by Th46;
hence  [y,x] nin inversions R by Th46; ::_thesis: verum
end;

theorem Th50: :: EXCHSORT:50
for x, y, z being set
for O being non empty connected Poset
for R being array of O st [x,y] in inversions R & [y,z] in inversions R holds
[x,z] in inversions R
proof
let x, y, z be set ; ::_thesis: for O being non empty connected Poset
for R being array of O st [x,y] in inversions R & [y,z] in inversions R holds
[x,z] in inversions R
let O be non empty connected Poset; ::_thesis: for R being array of O st [x,y] in inversions R & [y,z] in inversions R holds
[x,z] in inversions R
let R be array of O; ::_thesis: ( [x,y] in inversions R & [y,z] in inversions R implies [x,z] in inversions R )
assume A1: ( [x,y] in inversions R & [y,z] in inversions R ) ; ::_thesis: [x,z] in inversions R
then reconsider x = x, y = y, z = z as Element of dom R by Th46;
 ( x in y & R /. x > R /. y & y in z & R /. y > R /. z ) by A1, Th46;
then  ( x in z & R /. x > R /. z ) by ORDERS_2:5, ORDINAL1:10;
hence  [x,z] in inversions R ; ::_thesis: verum
end;

registration
let O be non empty connected Poset;
let R be array of O;
cluster inversions R ->  Relation-like ;
coherence
 inversions R is Relation-like
proof
 inversions R c= [:(dom R),(dom R):] by Th47;
hence  inversions R is Relation-like ; ::_thesis: verum
end;
end;

registration
let O be non empty connected Poset;
let R be array of O;
cluster inversions R ->  asymmetric transitive for Relation;
coherence
 for b1 being Relation st b1 = inversions R holds
( b1 is asymmetric & b1 is transitive )
proof
let r be Relation; ::_thesis: ( r = inversions R implies ( r is asymmetric & r is transitive ) )
assume A1: r = inversions R ; ::_thesis: ( r is asymmetric & r is transitive )
thus  r is asymmetric ::_thesis: r is transitive
proof
let x be set ; :: according to RELAT_2:def_5,RELAT_2:def_13 ::_thesis: for b1 being set holds
( not x in field r or not b1 in field r or not [x,b1] in r or not [b1,x] in r )
let y be set ; ::_thesis: ( not x in field r or not y in field r or not [x,y] in r or not [y,x] in r )
thus  ( not x in field r or not y in field r or not [x,y] in r or not [y,x] in r ) by A1, Th49; ::_thesis: verum
end;
let x be set ; :: according to RELAT_2:def_8,RELAT_2:def_16 ::_thesis: for b1, b2 being set holds
( not x in field r or not b1 in field r or not b2 in field r or not [x,b1] in r or not [b1,b2] in r or [x,b2] in r )
let y be set ; ::_thesis: for b1 being set holds
( not x in field r or not y in field r or not b1 in field r or not [x,y] in r or not [y,b1] in r or [x,b1] in r )
thus  for b1 being set holds
( not x in field r or not y in field r or not b1 in field r or not [x,y] in r or not [y,b1] in r or [x,b1] in r ) by A1, Th50; ::_thesis: verum
end;
end;

definition
let O be non empty connected Poset;
let a, b be Element of O;
:: original: <
redefine preda < b;
asymmetry
 for a, b being Element of O st R71(O,b1,b2) holds
not R71(O,b2,b1) by ORDERS_2:5;
end;

theorem Th51: :: EXCHSORT:51
for x, y being set
for O being non empty connected Poset
for R being array of O st [x,y] in inversions R holds
[x,y] nin inversions (Swap (R,x,y))
proof
let x, y be set ; ::_thesis: for O being non empty connected Poset
for R being array of O st [x,y] in inversions R holds
[x,y] nin inversions (Swap (R,x,y))
let O be non empty connected Poset; ::_thesis: for R being array of O st [x,y] in inversions R holds
[x,y] nin inversions (Swap (R,x,y))
let R be array of O; ::_thesis: ( [x,y] in inversions R implies [x,y] nin inversions (Swap (R,x,y)) )
assume A1: [x,y] in inversions R ; ::_thesis: [x,y] nin inversions (Swap (R,x,y))
then A2: ( x in dom R & y in dom R & R /. x > R /. y ) by Th46;
A3: not R /. x < R /. y by A1, Th46;
 ( (Swap (R,x,y)) /. x = R /. y & (Swap (R,x,y)) /. y = R /. x ) by A2, Th30, Th32;
hence  [x,y] nin inversions (Swap (R,x,y)) by A3, Th46; ::_thesis: verum
end;

theorem Th52: :: EXCHSORT:52
for x, y, z, t being set
for O being non empty connected Poset
for R being array of O st x in dom R & y in dom R & z <> x & z <> y & t <> x & t <> y holds
( [z,t] in inversions R iff [z,t] in inversions (Swap (R,x,y)) )
proof
let x, y, z, t be set ; ::_thesis: for O being non empty connected Poset
for R being array of O st x in dom R & y in dom R & z <> x & z <> y & t <> x & t <> y holds
( [z,t] in inversions R iff [z,t] in inversions (Swap (R,x,y)) )
let O be non empty connected Poset; ::_thesis: for R being array of O st x in dom R & y in dom R & z <> x & z <> y & t <> x & t <> y holds
( [z,t] in inversions R iff [z,t] in inversions (Swap (R,x,y)) )
let R be array of O; ::_thesis: ( x in dom R & y in dom R & z <> x & z <> y & t <> x & t <> y implies ( [z,t] in inversions R iff [z,t] in inversions (Swap (R,x,y)) ) )
set s = Swap (R,x,y);
assume  ( x in dom R & y in dom R & z <> x & z <> y & t <> x & t <> y ) ; ::_thesis: ( [z,t] in inversions R iff [z,t] in inversions (Swap (R,x,y)) )
then A1: ( ( z in dom R implies (Swap (R,x,y)) /. z = R /. z ) & ( t in dom R implies (Swap (R,x,y)) /. t = R /. t ) & dom (Swap (R,x,y)) = dom R ) by Th34, FUNCT_7:99;
hereby  ::_thesis: ( [z,t] in inversions (Swap (R,x,y)) implies [z,t] in inversions R )
assume  [z,t] in inversions R ; ::_thesis: [z,t] in inversions (Swap (R,x,y))
then  ( z in dom R & t in dom R & z in t & R /. z > R /. t ) by Th46;
hence  [z,t] in inversions (Swap (R,x,y)) by A1; ::_thesis: verum
end;
assume  [z,t] in inversions (Swap (R,x,y)) ; ::_thesis: [z,t] in inversions R
then  ( z in dom R & t in dom R & z in t & (Swap (R,x,y)) /. z > (Swap (R,x,y)) /. t ) by A1, Th46;
hence  [z,t] in inversions R by A1; ::_thesis: verum
end;

theorem Th53: :: EXCHSORT:53
for x, y, z being set
for O being non empty connected Poset
for R being array of O st [x,y] in inversions R holds
( ( [z,y] in inversions R & z in x ) iff [z,x] in inversions (Swap (R,x,y)) )
proof
let x, y, z be set ; ::_thesis: for O being non empty connected Poset
for R being array of O st [x,y] in inversions R holds
( ( [z,y] in inversions R & z in x ) iff [z,x] in inversions (Swap (R,x,y)) )
let O be non empty connected Poset; ::_thesis: for R being array of O st [x,y] in inversions R holds
( ( [z,y] in inversions R & z in x ) iff [z,x] in inversions (Swap (R,x,y)) )
let R be array of O; ::_thesis: ( [x,y] in inversions R implies ( ( [z,y] in inversions R & z in x ) iff [z,x] in inversions (Swap (R,x,y)) ) )
set s = Swap (R,x,y);
assume  [x,y] in inversions R ; ::_thesis: ( ( [z,y] in inversions R & z in x ) iff [z,x] in inversions (Swap (R,x,y)) )
then A1: ( x in dom R & y in dom R & x in y & R /. x > R /. y ) by Th46;
then A2: ( (Swap (R,x,y)) /. x = R /. y & (Swap (R,x,y)) /. y = R /. x & dom (Swap (R,x,y)) = dom R ) by Th30, Th32, FUNCT_7:99;
hereby  ::_thesis: ( [z,x] in inversions (Swap (R,x,y)) implies ( [z,y] in inversions R & z in x ) )
assume A3: ( [z,y] in inversions R & z in x ) ; ::_thesis: [z,x] in inversions (Swap (R,x,y))
then A4: ( z in dom R & z in y & R /. z > R /. y ) by Th46;
then  ( x <> z & y <> z ) by A3;
then  (Swap (R,x,y)) /. z = R /. z by A4, Th34;
hence  [z,x] in inversions (Swap (R,x,y)) by A3, A1, A2, A4; ::_thesis: verum
end;
assume  [z,x] in inversions (Swap (R,x,y)) ; ::_thesis: ( [z,y] in inversions R & z in x )
then A5: ( z in dom R & z in x & (Swap (R,x,y)) /. z > (Swap (R,x,y)) /. x ) by A2, Th46;
then A6: z in y by A1, ORDINAL1:10;
 (Swap (R,x,y)) /. z = R /. z by A1, A5, Th34;
hence  ( [z,y] in inversions R & z in x ) by A1, A2, A5, A6; ::_thesis: verum
end;

theorem Th54: :: EXCHSORT:54
for x, y, z being set
for O being non empty connected Poset
for R being array of O st [x,y] in inversions R holds
( [z,x] in inversions R iff ( z in x & [z,y] in inversions (Swap (R,x,y)) ) )
proof
let x, y, z be set ; ::_thesis: for O being non empty connected Poset
for R being array of O st [x,y] in inversions R holds
( [z,x] in inversions R iff ( z in x & [z,y] in inversions (Swap (R,x,y)) ) )
let O be non empty connected Poset; ::_thesis: for R being array of O st [x,y] in inversions R holds
( [z,x] in inversions R iff ( z in x & [z,y] in inversions (Swap (R,x,y)) ) )
let R be array of O; ::_thesis: ( [x,y] in inversions R implies ( [z,x] in inversions R iff ( z in x & [z,y] in inversions (Swap (R,x,y)) ) ) )
assume  [x,y] in inversions R ; ::_thesis: ( [z,x] in inversions R iff ( z in x & [z,y] in inversions (Swap (R,x,y)) ) )
then A1: ( x in dom R & y in dom R & x in y & R /. x > R /. y ) by Th46;
A2: dom (Swap (R,x,y)) = dom R by FUNCT_7:99;
hereby  ::_thesis: ( z in x & [z,y] in inversions (Swap (R,x,y)) implies [z,x] in inversions R )
assume  [z,x] in inversions R ; ::_thesis: ( z in x & [z,y] in inversions (Swap (R,x,y)) )
then A3: ( z in dom R & z in x & R /. z > R /. x ) by Th46;
then A4: z in y by A1, ORDINAL1:10;
 ( (Swap (R,x,y)) /. y = R /. x & (Swap (R,x,y)) /. z = R /. z ) by A1, A3, Th32, Th34;
hence  ( z in x & [z,y] in inversions (Swap (R,x,y)) ) by A1, A2, A3, A4; ::_thesis: verum
end;
assume A5: ( z in x & [z,y] in inversions (Swap (R,x,y)) ) ; ::_thesis: [z,x] in inversions R
then A6: ( z in dom R & z in y & (Swap (R,x,y)) /. z > (Swap (R,x,y)) /. y ) by A2, Th46;
then  ( z <> x & z <> y ) by A5;
then  ( (Swap (R,x,y)) /. y = R /. x & (Swap (R,x,y)) /. z = R /. z ) by A1, A6, Th32, Th34;
hence  [z,x] in inversions R by A1, A6, A5; ::_thesis: verum
end;

theorem Th55: :: EXCHSORT:55
for x, y, z being set
for O being non empty connected Poset
for R being array of O st [x,y] in inversions R & z in y & [x,z] in inversions (Swap (R,x,y)) holds
[x,z] in inversions R
proof
let x, y, z be set ; ::_thesis: for O being non empty connected Poset
for R being array of O st [x,y] in inversions R & z in y & [x,z] in inversions (Swap (R,x,y)) holds
[x,z] in inversions R
let O be non empty connected Poset; ::_thesis: for R being array of O st [x,y] in inversions R & z in y & [x,z] in inversions (Swap (R,x,y)) holds
[x,z] in inversions R
let R be array of O; ::_thesis: ( [x,y] in inversions R & z in y & [x,z] in inversions (Swap (R,x,y)) implies [x,z] in inversions R )
assume  [x,y] in inversions R ; ::_thesis: ( not z in y or not [x,z] in inversions (Swap (R,x,y)) or [x,z] in inversions R )
then A1: ( x in dom R & y in dom R & x in y & R /. x > R /. y ) by Th46;
A2: dom (Swap (R,x,y)) = dom R by FUNCT_7:99;
assume A3: z in y ; ::_thesis: ( not [x,z] in inversions (Swap (R,x,y)) or [x,z] in inversions R )
assume  [x,z] in inversions (Swap (R,x,y)) ; ::_thesis: [x,z] in inversions R
then A4: ( z in dom R & x in z & (Swap (R,x,y)) /. x > (Swap (R,x,y)) /. z ) by A2, Th46;
then  ( z <> x & z <> y ) by A3;
then  ( (Swap (R,x,y)) /. x = R /. y & (Swap (R,x,y)) /. z = R /. z ) by A1, A4, Th30, Th34;
then  R /. x > R /. z by A1, A4, ORDERS_2:5;
hence  [x,z] in inversions R by A1, A4; ::_thesis: verum
end;

theorem Th56: :: EXCHSORT:56
for x, y, z being set
for O being non empty connected Poset
for R being array of O st [x,y] in inversions R & x in z & [z,y] in inversions (Swap (R,x,y)) holds
[z,y] in inversions R
proof
let x, y, z be set ; ::_thesis: for O being non empty connected Poset
for R being array of O st [x,y] in inversions R & x in z & [z,y] in inversions (Swap (R,x,y)) holds
[z,y] in inversions R
let O be non empty connected Poset; ::_thesis: for R being array of O st [x,y] in inversions R & x in z & [z,y] in inversions (Swap (R,x,y)) holds
[z,y] in inversions R
let R be array of O; ::_thesis: ( [x,y] in inversions R & x in z & [z,y] in inversions (Swap (R,x,y)) implies [z,y] in inversions R )
assume  [x,y] in inversions R ; ::_thesis: ( not x in z or not [z,y] in inversions (Swap (R,x,y)) or [z,y] in inversions R )
then A1: ( x in dom R & y in dom R & x in y & R /. x > R /. y ) by Th46;
A2: dom (Swap (R,x,y)) = dom R by FUNCT_7:99;
assume A3: x in z ; ::_thesis: ( not [z,y] in inversions (Swap (R,x,y)) or [z,y] in inversions R )
assume  [z,y] in inversions (Swap (R,x,y)) ; ::_thesis: [z,y] in inversions R
then A4: ( z in dom R & z in y & (Swap (R,x,y)) /. z > (Swap (R,x,y)) /. y ) by A2, Th46;
then  ( z <> x & z <> y ) by A3;
then  ( (Swap (R,x,y)) /. y = R /. x & (Swap (R,x,y)) /. z = R /. z ) by A1, A4, Th32, Th34;
then  R /. z > R /. y by A1, A4, ORDERS_2:5;
hence  [z,y] in inversions R by A1, A4; ::_thesis: verum
end;

theorem Th57: :: EXCHSORT:57
for x, y, z being set
for O being non empty connected Poset
for R being array of O st [x,y] in inversions R & y in z & [x,z] in inversions (Swap (R,x,y)) holds
[y,z] in inversions R
proof
let x, y, z be set ; ::_thesis: for O being non empty connected Poset
for R being array of O st [x,y] in inversions R & y in z & [x,z] in inversions (Swap (R,x,y)) holds
[y,z] in inversions R
let O be non empty connected Poset; ::_thesis: for R being array of O st [x,y] in inversions R & y in z & [x,z] in inversions (Swap (R,x,y)) holds
[y,z] in inversions R
let R be array of O; ::_thesis: ( [x,y] in inversions R & y in z & [x,z] in inversions (Swap (R,x,y)) implies [y,z] in inversions R )
assume  [x,y] in inversions R ; ::_thesis: ( not y in z or not [x,z] in inversions (Swap (R,x,y)) or [y,z] in inversions R )
then A1: ( x in dom R & y in dom R & x in y & R /. x > R /. y ) by Th46;
A2: dom (Swap (R,x,y)) = dom R by FUNCT_7:99;
assume A3: y in z ; ::_thesis: ( not [x,z] in inversions (Swap (R,x,y)) or [y,z] in inversions R )
assume  [x,z] in inversions (Swap (R,x,y)) ; ::_thesis: [y,z] in inversions R
then A4: ( z in dom R & x in z & (Swap (R,x,y)) /. x > (Swap (R,x,y)) /. z ) by A2, Th46;
then  ( z <> x & z <> y ) by A3;
then  ( (Swap (R,x,y)) /. x = R /. y & (Swap (R,x,y)) /. z = R /. z ) by A1, A4, Th30, Th34;
hence  [y,z] in inversions R by A1, A4, A3; ::_thesis: verum
end;

theorem Th58: :: EXCHSORT:58
for x, y, z being set
for O being non empty connected Poset
for R being array of O st [x,y] in inversions R holds
( ( y in z & [x,z] in inversions R ) iff [y,z] in inversions (Swap (R,x,y)) )
proof
let x, y, z be set ; ::_thesis: for O being non empty connected Poset
for R being array of O st [x,y] in inversions R holds
( ( y in z & [x,z] in inversions R ) iff [y,z] in inversions (Swap (R,x,y)) )
let O be non empty connected Poset; ::_thesis: for R being array of O st [x,y] in inversions R holds
( ( y in z & [x,z] in inversions R ) iff [y,z] in inversions (Swap (R,x,y)) )
let R be array of O; ::_thesis: ( [x,y] in inversions R implies ( ( y in z & [x,z] in inversions R ) iff [y,z] in inversions (Swap (R,x,y)) ) )
assume  [x,y] in inversions R ; ::_thesis: ( ( y in z & [x,z] in inversions R ) iff [y,z] in inversions (Swap (R,x,y)) )
then A1: ( x in dom R & y in dom R & x in y & R /. x > R /. y ) by Th46;
A2: dom (Swap (R,x,y)) = dom R by FUNCT_7:99;
hereby  ::_thesis: ( [y,z] in inversions (Swap (R,x,y)) implies ( y in z & [x,z] in inversions R ) )
assume A3: ( y in z & [x,z] in inversions R ) ; ::_thesis: [y,z] in inversions (Swap (R,x,y))
then A4: ( z in dom R & x in z & R /. z < R /. x ) by Th46;
then  ( z <> x & z <> y ) by A3;
then  ( (Swap (R,x,y)) /. y = R /. x & (Swap (R,x,y)) /. z = R /. z ) by A1, A4, Th32, Th34;
hence  [y,z] in inversions (Swap (R,x,y)) by A1, A2, A4, A3; ::_thesis: verum
end;
assume  [y,z] in inversions (Swap (R,x,y)) ; ::_thesis: ( y in z & [x,z] in inversions R )
then A5: ( z in dom R & y in z & (Swap (R,x,y)) /. y > (Swap (R,x,y)) /. z ) by A2, Th46;
then A6: x in z by A1, ORDINAL1:10;
 ( (Swap (R,x,y)) /. y = R /. x & (Swap (R,x,y)) /. z = R /. z ) by A1, Th32, Th34, A5;
hence  ( y in z & [x,z] in inversions R ) by A1, A5, A6; ::_thesis: verum
end;

definition
let O be non empty connected Poset;
let R be array of O;
let x, y be set ;
func(R,x,y) incl  ->  Function equals :: EXCHSORT:def 13
[:(Swap ((id (dom R)),x,y)),(Swap ((id (dom R)),x,y)):] +* (id ([:{x},((succ y) \ x):] \/ [:((succ y) \ x),{y}:]));
coherence
 [:(Swap ((id (dom R)),x,y)),(Swap ((id (dom R)),x,y)):] +* (id ([:{x},((succ y) \ x):] \/ [:((succ y) \ x),{y}:])) is Function ;
end;

:: deftheorem  defines incl EXCHSORT:def_13_:_
 for O being non empty connected Poset
for R being array of O
for x, y being set holds (R,x,y) incl = [:(Swap ((id (dom R)),x,y)),(Swap ((id (dom R)),x,y)):] +* (id ([:{x},((succ y) \ x):] \/ [:((succ y) \ x),{y}:]));

theorem Th59: :: EXCHSORT:59
for c, b, a being ordinal number holds
( c in (succ b) \ a iff ( a c= c & c c= b ) )
proof
let c, b, a be ordinal number ; ::_thesis: ( c in (succ b) \ a iff ( a c= c & c c= b ) )
 ( a c= c iff c nin a ) by ORDINAL6:4;
then  ( c in (succ b) \ a iff ( c in succ b & a c= c ) ) by XBOOLE_0:def_5;
hence  ( c in (succ b) \ a iff ( a c= c & c c= b ) ) by ORDINAL1:22; ::_thesis: verum
end;


theorem Th60: :: EXCHSORT:60
for O being non empty connected Poset
for T being non empty array of O
for q, p being Element of dom T holds (succ q) \ p c= dom T
proof
let O be non empty connected Poset; ::_thesis: for T being non empty array of O
for q, p being Element of dom T holds (succ q) \ p c= dom T
let T be non empty array of O; ::_thesis: for q, p being Element of dom T holds (succ q) \ p c= dom T
let q, p be Element of dom T; ::_thesis: (succ q) \ p c= dom T
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (succ q) \ p or x in dom T )
assume A1: x in (succ q) \ p ; ::_thesis: x in dom T
A2: ( p c= x & x c= q ) by A1, Th59;
consider a, b being ordinal number  such that
A3: dom T = a \ b by Def1;
 ( q in a & p nin b ) by A3, XBOOLE_0:def_5;
then  ( x in a & x nin b ) by A1, A2, ORDINAL1:12;
hence  x in dom T by A3, XBOOLE_0:def_5; ::_thesis: verum
end;

theorem Th61: :: EXCHSORT:61
for O being non empty connected Poset
for T being non empty array of O
for p, q being Element of dom T holds
( dom ((T,p,q) incl) = [:(dom T),(dom T):] & rng ((T,p,q) incl) c= [:(dom T),(dom T):] )
proof
let O be non empty connected Poset; ::_thesis: for T being non empty array of O
for p, q being Element of dom T holds
( dom ((T,p,q) incl) = [:(dom T),(dom T):] & rng ((T,p,q) incl) c= [:(dom T),(dom T):] )
let T be non empty array of O; ::_thesis: for p, q being Element of dom T holds
( dom ((T,p,q) incl) = [:(dom T),(dom T):] & rng ((T,p,q) incl) c= [:(dom T),(dom T):] )
let p, q be Element of dom T; ::_thesis: ( dom ((T,p,q) incl) = [:(dom T),(dom T):] & rng ((T,p,q) incl) c= [:(dom T),(dom T):] )
set X = dom T;
set i = id (dom T);
set s = Swap ((id (dom T)),p,q);
set f = [:(Swap ((id (dom T)),p,q)),(Swap ((id (dom T)),p,q)):];
set Y = (succ q) \ p;
set Z1 = [:{p},((succ q) \ p):];
set Z2 = [:((succ q) \ p),{q}:];
set g = id ([:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:]);
 dom (id (dom T)) = dom T ;
then A1: dom (Swap ((id (dom T)),p,q)) = dom T by FUNCT_7:99;
A2: ( {p} c= dom T & {q} c= dom T & (succ q) \ p c= dom T ) by Th60, ZFMISC_1:31;
A3: [:(dom T),(dom T):] \/ ([:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:]) = ([:(dom T),(dom T):] \/ [:{p},((succ q) \ p):]) \/ [:((succ q) \ p),{q}:] by XBOOLE_1:4
.= [:(dom T),(dom T):] \/ [:((succ q) \ p),{q}:] by A2, XBOOLE_1:12, ZFMISC_1:96
.= [:(dom T),(dom T):] by A2, XBOOLE_1:12, ZFMISC_1:96 ;
thus  dom ((T,p,q) incl) = (dom [:(Swap ((id (dom T)),p,q)),(Swap ((id (dom T)),p,q)):]) \/ (dom (id ([:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:]))) by FUNCT_4:def_1
.= (dom [:(Swap ((id (dom T)),p,q)),(Swap ((id (dom T)),p,q)):]) \/ ([:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:])
.= [:(dom T),(dom T):] by A1, A3, FUNCT_3:def_8 ; ::_thesis: rng ((T,p,q) incl) c= [:(dom T),(dom T):]
A4: ( rng (id ([:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:])) = [:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:] & rng (id (dom T)) = dom T ) ;
 rng (Swap ((id (dom T)),p,q)) = dom T by A4, FUNCT_7:103;
then  rng [:(Swap ((id (dom T)),p,q)),(Swap ((id (dom T)),p,q)):] = [:(dom T),(dom T):] by FUNCT_3:67;
hence  rng ((T,p,q) incl) c= [:(dom T),(dom T):] by A3, A4, FUNCT_4:17; ::_thesis: verum
end;

theorem Th62: :: EXCHSORT:62
for O being non empty connected Poset
for T being non empty array of O
for p, r, q being Element of dom T st p c= r & r c= q holds
( ((T,p,q) incl) . (p,r) = [p,r] & ((T,p,q) incl) . (r,q) = [r,q] )
proof
let O be non empty connected Poset; ::_thesis: for T being non empty array of O
for p, r, q being Element of dom T st p c= r & r c= q holds
( ((T,p,q) incl) . (p,r) = [p,r] & ((T,p,q) incl) . (r,q) = [r,q] )
let T be non empty array of O; ::_thesis: for p, r, q being Element of dom T st p c= r & r c= q holds
( ((T,p,q) incl) . (p,r) = [p,r] & ((T,p,q) incl) . (r,q) = [r,q] )
let p, r, q be Element of dom T; ::_thesis: ( p c= r & r c= q implies ( ((T,p,q) incl) . (p,r) = [p,r] & ((T,p,q) incl) . (r,q) = [r,q] ) )
assume A1: ( p c= r & r c= q ) ; ::_thesis: ( ((T,p,q) incl) . (p,r) = [p,r] & ((T,p,q) incl) . (r,q) = [r,q] )
set Y = (succ q) \ p;
set Z1 = [:{p},((succ q) \ p):];
set Z2 = [:((succ q) \ p),{q}:];
set g = id ([:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:]);
 ( p in {p} & q in {q} & r in (succ q) \ p ) by A1, Th59, TARSKI:def_1;
then  ( [p,r] in [:{p},((succ q) \ p):] & [r,q] in [:((succ q) \ p),{q}:] ) by ZFMISC_1:def_2;
then A2: ( [p,r] in [:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:] & [r,q] in [:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:] ) by XBOOLE_0:def_3;
A3: dom (id ([:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:])) = [:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:] ;
hence ((T,p,q) incl) . (p,r) = (id ([:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:])) . (p,r) by A2, FUNCT_4:13
.= [p,r] by A2, FUNCT_1:17 ;
::_thesis: ((T,p,q) incl) . (r,q) = [r,q]
thus ((T,p,q) incl) . (r,q) = (id ([:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:])) . (r,q) by A2, A3, FUNCT_4:13
.= [r,q] by A2, FUNCT_1:17 ; ::_thesis: verum
end;

theorem Th63: :: EXCHSORT:63
for f being Function
for O being non empty connected Poset
for T being non empty array of O
for r, p, s, q being Element of dom T st r <> p & s <> q & f = Swap ((id (dom T)),p,q) holds
((T,p,q) incl) . (r,s) = [(f . r),(f . s)]
proof
let f be Function; ::_thesis: for O being non empty connected Poset
for T being non empty array of O
for r, p, s, q being Element of dom T st r <> p & s <> q & f = Swap ((id (dom T)),p,q) holds
((T,p,q) incl) . (r,s) = [(f . r),(f . s)]
let O be non empty connected Poset; ::_thesis: for T being non empty array of O
for r, p, s, q being Element of dom T st r <> p & s <> q & f = Swap ((id (dom T)),p,q) holds
((T,p,q) incl) . (r,s) = [(f . r),(f . s)]
let T be non empty array of O; ::_thesis: for r, p, s, q being Element of dom T st r <> p & s <> q & f = Swap ((id (dom T)),p,q) holds
((T,p,q) incl) . (r,s) = [(f . r),(f . s)]
let r, p, s, q be Element of dom T; ::_thesis: ( r <> p & s <> q & f = Swap ((id (dom T)),p,q) implies ((T,p,q) incl) . (r,s) = [(f . r),(f . s)] )
assume that
A1: ( r <> p & s <> q ) and
A2: f = Swap ((id (dom T)),p,q) ; ::_thesis: ((T,p,q) incl) . (r,s) = [(f . r),(f . s)]
set Y = (succ q) \ p;
set Z1 = [:{p},((succ q) \ p):];
set Z2 = [:((succ q) \ p),{q}:];
set g = id ([:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:]);
A3: dom f = dom (id (dom T)) by A2, FUNCT_7:99
.= dom T ;
 ( r nin {p} & s nin {q} ) by A1, TARSKI:def_1;
then  ( [r,s] nin [:{p},((succ q) \ p):] & [r,s] nin [:((succ q) \ p),{q}:] ) by ZFMISC_1:87;
then  [r,s] nin dom (id ([:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:])) by XBOOLE_0:def_3;
hence ((T,p,q) incl) . (r,s) = [:f,f:] . (r,s) by A2, FUNCT_4:11
.= [(f . r),(f . s)] by A3, FUNCT_3:def_8 ;
::_thesis: verum
end;

theorem Th64: :: EXCHSORT:64
for f being Function
for O being non empty connected Poset
for T being non empty array of O
for r, p, q being Element of dom T st r in p & f = Swap ((id (dom T)),p,q) holds
( ((T,p,q) incl) . (r,q) = [(f . r),(f . q)] & ((T,p,q) incl) . (r,p) = [(f . r),(f . p)] )
proof
let f be Function; ::_thesis: for O being non empty connected Poset
for T being non empty array of O
for r, p, q being Element of dom T st r in p & f = Swap ((id (dom T)),p,q) holds
( ((T,p,q) incl) . (r,q) = [(f . r),(f . q)] & ((T,p,q) incl) . (r,p) = [(f . r),(f . p)] )
let O be non empty connected Poset; ::_thesis: for T being non empty array of O
for r, p, q being Element of dom T st r in p & f = Swap ((id (dom T)),p,q) holds
( ((T,p,q) incl) . (r,q) = [(f . r),(f . q)] & ((T,p,q) incl) . (r,p) = [(f . r),(f . p)] )
let T be non empty array of O; ::_thesis: for r, p, q being Element of dom T st r in p & f = Swap ((id (dom T)),p,q) holds
( ((T,p,q) incl) . (r,q) = [(f . r),(f . q)] & ((T,p,q) incl) . (r,p) = [(f . r),(f . p)] )
let r, p, q be Element of dom T; ::_thesis: ( r in p & f = Swap ((id (dom T)),p,q) implies ( ((T,p,q) incl) . (r,q) = [(f . r),(f . q)] & ((T,p,q) incl) . (r,p) = [(f . r),(f . p)] ) )
assume that
A1: r in p and
A2: f = Swap ((id (dom T)),p,q) ; ::_thesis: ( ((T,p,q) incl) . (r,q) = [(f . r),(f . q)] & ((T,p,q) incl) . (r,p) = [(f . r),(f . p)] )
set X = dom T;
set i = id (dom T);
set s = Swap ((id (dom T)),p,q);
set h = [:(Swap ((id (dom T)),p,q)),(Swap ((id (dom T)),p,q)):];
set Y = (succ q) \ p;
set Z1 = [:{p},((succ q) \ p):];
set Z2 = [:((succ q) \ p),{q}:];
set g = id ([:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:]);
 dom (id (dom T)) = dom T ;
then A3: dom (Swap ((id (dom T)),p,q)) = dom T by FUNCT_7:99;
 not p c= r by A1, ORDINAL6:4;
then  ( r nin {p} & r nin (succ q) \ p ) by Th59, TARSKI:def_1;
then  ( [r,p] nin [:{p},((succ q) \ p):] & [r,p] nin [:((succ q) \ p),{q}:] & [r,q] nin [:{p},((succ q) \ p):] & [r,q] nin [:((succ q) \ p),{q}:] ) by ZFMISC_1:87;
then A4: ( [r,q] nin dom (id ([:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:])) & [r,p] nin dom (id ([:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:])) ) by XBOOLE_0:def_3;
hence ((T,p,q) incl) . (r,q) = [:(Swap ((id (dom T)),p,q)),(Swap ((id (dom T)),p,q)):] . (r,q) by FUNCT_4:11
.= [(f . r),(f . q)] by A2, A3, FUNCT_3:def_8 ;
::_thesis: ((T,p,q) incl) . (r,p) = [(f . r),(f . p)]
thus ((T,p,q) incl) . (r,p) = [:(Swap ((id (dom T)),p,q)),(Swap ((id (dom T)),p,q)):] . (r,p) by A4, FUNCT_4:11
.= [(f . r),(f . p)] by A2, A3, FUNCT_3:def_8 ; ::_thesis: verum
end;

theorem Th65: :: EXCHSORT:65
for f being Function
for O being non empty connected Poset
for T being non empty array of O
for q, r, p being Element of dom T st q in r & f = Swap ((id (dom T)),p,q) holds
( ((T,p,q) incl) . (p,r) = [(f . p),(f . r)] & ((T,p,q) incl) . (q,r) = [(f . q),(f . r)] )
proof
let f be Function; ::_thesis: for O being non empty connected Poset
for T being non empty array of O
for q, r, p being Element of dom T st q in r & f = Swap ((id (dom T)),p,q) holds
( ((T,p,q) incl) . (p,r) = [(f . p),(f . r)] & ((T,p,q) incl) . (q,r) = [(f . q),(f . r)] )
let O be non empty connected Poset; ::_thesis: for T being non empty array of O
for q, r, p being Element of dom T st q in r & f = Swap ((id (dom T)),p,q) holds
( ((T,p,q) incl) . (p,r) = [(f . p),(f . r)] & ((T,p,q) incl) . (q,r) = [(f . q),(f . r)] )
let T be non empty array of O; ::_thesis: for q, r, p being Element of dom T st q in r & f = Swap ((id (dom T)),p,q) holds
( ((T,p,q) incl) . (p,r) = [(f . p),(f . r)] & ((T,p,q) incl) . (q,r) = [(f . q),(f . r)] )
let q, r, p be Element of dom T; ::_thesis: ( q in r & f = Swap ((id (dom T)),p,q) implies ( ((T,p,q) incl) . (p,r) = [(f . p),(f . r)] & ((T,p,q) incl) . (q,r) = [(f . q),(f . r)] ) )
assume that
A1: q in r and
A2: f = Swap ((id (dom T)),p,q) ; ::_thesis: ( ((T,p,q) incl) . (p,r) = [(f . p),(f . r)] & ((T,p,q) incl) . (q,r) = [(f . q),(f . r)] )
set X = dom T;
set i = id (dom T);
set s = Swap ((id (dom T)),p,q);
set h = [:(Swap ((id (dom T)),p,q)),(Swap ((id (dom T)),p,q)):];
set Y = (succ q) \ p;
set Z1 = [:{p},((succ q) \ p):];
set Z2 = [:((succ q) \ p),{q}:];
set g = id ([:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:]);
 dom (id (dom T)) = dom T ;
then A3: dom (Swap ((id (dom T)),p,q)) = dom T by FUNCT_7:99;
 not r c= q by A1, ORDINAL6:4;
then  ( r nin {q} & r nin (succ q) \ p ) by Th59, TARSKI:def_1;
then  ( [p,r] nin [:{p},((succ q) \ p):] & [p,r] nin [:((succ q) \ p),{q}:] & [q,r] nin [:{p},((succ q) \ p):] & [q,r] nin [:((succ q) \ p),{q}:] ) by ZFMISC_1:87;
then A4: ( [p,r] nin dom (id ([:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:])) & [q,r] nin dom (id ([:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:])) ) by XBOOLE_0:def_3;
hence ((T,p,q) incl) . (p,r) = [:(Swap ((id (dom T)),p,q)),(Swap ((id (dom T)),p,q)):] . (p,r) by FUNCT_4:11
.= [(f . p),(f . r)] by A2, A3, FUNCT_3:def_8 ;
::_thesis: ((T,p,q) incl) . (q,r) = [(f . q),(f . r)]
thus ((T,p,q) incl) . (q,r) = [:(Swap ((id (dom T)),p,q)),(Swap ((id (dom T)),p,q)):] . (q,r) by A4, FUNCT_4:11
.= [(f . q),(f . r)] by A2, A3, FUNCT_3:def_8 ; ::_thesis: verum
end;

theorem Th66: :: EXCHSORT:66
for O being non empty connected Poset
for T being non empty array of O
for p, q being Element of dom T st p in q holds
((T,p,q) incl) . (p,q) = [p,q]
proof
let O be non empty connected Poset; ::_thesis: for T being non empty array of O
for p, q being Element of dom T st p in q holds
((T,p,q) incl) . (p,q) = [p,q]
let T be non empty array of O; ::_thesis: for p, q being Element of dom T st p in q holds
((T,p,q) incl) . (p,q) = [p,q]
let p, q be Element of dom T; ::_thesis: ( p in q implies ((T,p,q) incl) . (p,q) = [p,q] )
assume  p in q ; ::_thesis: ((T,p,q) incl) . (p,q) = [p,q]
then  p c= q by ORDINAL1:def_2;
hence  ((T,p,q) incl) . (p,q) = [p,q] by Th62; ::_thesis: verum
end;

theorem Th67: :: EXCHSORT:67
for O being non empty connected Poset
for T being non empty array of O
for p, q, r, s being Element of dom T st p in q & r <> p & r <> q & s <> p & s <> q holds
((T,p,q) incl) . (r,s) = [r,s]
proof
let O be non empty connected Poset; ::_thesis: for T being non empty array of O
for p, q, r, s being Element of dom T st p in q & r <> p & r <> q & s <> p & s <> q holds
((T,p,q) incl) . (r,s) = [r,s]
let T be non empty array of O; ::_thesis: for p, q, r, s being Element of dom T st p in q & r <> p & r <> q & s <> p & s <> q holds
((T,p,q) incl) . (r,s) = [r,s]
let p, q, r, s be Element of dom T; ::_thesis: ( p in q & r <> p & r <> q & s <> p & s <> q implies ((T,p,q) incl) . (r,s) = [r,s] )
assume A1: ( p in q & r <> p & r <> q & s <> p & s <> q ) ; ::_thesis: ((T,p,q) incl) . (r,s) = [r,s]
set X = dom T;
set i = id (dom T);
set f = Swap ((id (dom T)),p,q);
set h = [:(Swap ((id (dom T)),p,q)),(Swap ((id (dom T)),p,q)):];
set Y = (succ q) \ p;
thus ((T,p,q) incl) . (r,s) = [((Swap ((id (dom T)),p,q)) . r),((Swap ((id (dom T)),p,q)) . s)] by A1, Th63
.= [((id (dom T)) . r),((Swap ((id (dom T)),p,q)) . s)] by A1, Th33
.= [((id (dom T)) . r),((id (dom T)) . s)] by A1, Th33
.= [r,((id (dom T)) . s)] by FUNCT_1:17
.= [r,s] by FUNCT_1:17 ; ::_thesis: verum
end;

theorem Th68: :: EXCHSORT:68
for O being non empty connected Poset
for T being non empty array of O
for r, p, q being Element of dom T st r in p & p in q holds
( ((T,p,q) incl) . (r,p) = [r,q] & ((T,p,q) incl) . (r,q) = [r,p] )
proof
let O be non empty connected Poset; ::_thesis: for T being non empty array of O
for r, p, q being Element of dom T st r in p & p in q holds
( ((T,p,q) incl) . (r,p) = [r,q] & ((T,p,q) incl) . (r,q) = [r,p] )
let T be non empty array of O; ::_thesis: for r, p, q being Element of dom T st r in p & p in q holds
( ((T,p,q) incl) . (r,p) = [r,q] & ((T,p,q) incl) . (r,q) = [r,p] )
let r, p, q be Element of dom T; ::_thesis: ( r in p & p in q implies ( ((T,p,q) incl) . (r,p) = [r,q] & ((T,p,q) incl) . (r,q) = [r,p] ) )
assume A1: ( r in p & p in q ) ; ::_thesis: ( ((T,p,q) incl) . (r,p) = [r,q] & ((T,p,q) incl) . (r,q) = [r,p] )
set X = dom T;
set i = id (dom T);
set f = Swap ((id (dom T)),p,q);
set h = [:(Swap ((id (dom T)),p,q)),(Swap ((id (dom T)),p,q)):];
set Y = (succ q) \ p;
A2: dom (id (dom T)) = dom T ;
A3: ( r <> p & r <> q ) by A1;
thus ((T,p,q) incl) . (r,p) = [((Swap ((id (dom T)),p,q)) . r),((Swap ((id (dom T)),p,q)) . p)] by A1, Th64
.= [((id (dom T)) . r),((Swap ((id (dom T)),p,q)) . p)] by A3, Th33
.= [r,((Swap ((id (dom T)),p,q)) . p)] by FUNCT_1:17
.= [r,((id (dom T)) . q)] by A2, Th29
.= [r,q] by FUNCT_1:17 ; ::_thesis: ((T,p,q) incl) . (r,q) = [r,p]
thus ((T,p,q) incl) . (r,q) = [((Swap ((id (dom T)),p,q)) . r),((Swap ((id (dom T)),p,q)) . q)] by A1, Th64
.= [((id (dom T)) . r),((Swap ((id (dom T)),p,q)) . q)] by A3, Th33
.= [r,((Swap ((id (dom T)),p,q)) . q)] by FUNCT_1:17
.= [r,((id (dom T)) . p)] by A2, Th31
.= [r,p] by FUNCT_1:17 ; ::_thesis: verum
end;

theorem Th69: :: EXCHSORT:69
for O being non empty connected Poset
for T being non empty array of O
for p, s, q being Element of dom T st p in s & s in q holds
( ((T,p,q) incl) . (p,s) = [p,s] & ((T,p,q) incl) . (s,q) = [s,q] )
proof
let O be non empty connected Poset; ::_thesis: for T being non empty array of O
for p, s, q being Element of dom T st p in s & s in q holds
( ((T,p,q) incl) . (p,s) = [p,s] & ((T,p,q) incl) . (s,q) = [s,q] )
let T be non empty array of O; ::_thesis: for p, s, q being Element of dom T st p in s & s in q holds
( ((T,p,q) incl) . (p,s) = [p,s] & ((T,p,q) incl) . (s,q) = [s,q] )
let p, s, q be Element of dom T; ::_thesis: ( p in s & s in q implies ( ((T,p,q) incl) . (p,s) = [p,s] & ((T,p,q) incl) . (s,q) = [s,q] ) )
assume  ( p in s & s in q ) ; ::_thesis: ( ((T,p,q) incl) . (p,s) = [p,s] & ((T,p,q) incl) . (s,q) = [s,q] )
then  ( p c= s & s c= q ) by ORDINAL1:def_2;
hence  ( ((T,p,q) incl) . (p,s) = [p,s] & ((T,p,q) incl) . (s,q) = [s,q] ) by Th62; ::_thesis: verum
end;

theorem Th70: :: EXCHSORT:70
for O being non empty connected Poset
for T being non empty array of O
for p, q, s being Element of dom T st p in q & q in s holds
( ((T,p,q) incl) . (p,s) = [q,s] & ((T,p,q) incl) . (q,s) = [p,s] )
proof
let O be non empty connected Poset; ::_thesis: for T being non empty array of O
for p, q, s being Element of dom T st p in q & q in s holds
( ((T,p,q) incl) . (p,s) = [q,s] & ((T,p,q) incl) . (q,s) = [p,s] )
let T be non empty array of O; ::_thesis: for p, q, s being Element of dom T st p in q & q in s holds
( ((T,p,q) incl) . (p,s) = [q,s] & ((T,p,q) incl) . (q,s) = [p,s] )
let p, q, s be Element of dom T; ::_thesis: ( p in q & q in s implies ( ((T,p,q) incl) . (p,s) = [q,s] & ((T,p,q) incl) . (q,s) = [p,s] ) )
assume A1: ( p in q & q in s ) ; ::_thesis: ( ((T,p,q) incl) . (p,s) = [q,s] & ((T,p,q) incl) . (q,s) = [p,s] )
set X = dom T;
set i = id (dom T);
set f = Swap ((id (dom T)),p,q);
set h = [:(Swap ((id (dom T)),p,q)),(Swap ((id (dom T)),p,q)):];
set Y = (succ q) \ p;
A2: dom (id (dom T)) = dom T ;
A3: ( s <> p & s <> q ) by A1;
thus ((T,p,q) incl) . (p,s) = [((Swap ((id (dom T)),p,q)) . p),((Swap ((id (dom T)),p,q)) . s)] by A1, Th65
.= [((Swap ((id (dom T)),p,q)) . p),((id (dom T)) . s)] by A3, Th33
.= [((Swap ((id (dom T)),p,q)) . p),s] by FUNCT_1:17
.= [((id (dom T)) . q),s] by A2, Th29
.= [q,s] by FUNCT_1:17 ; ::_thesis: ((T,p,q) incl) . (q,s) = [p,s]
thus ((T,p,q) incl) . (q,s) = [((Swap ((id (dom T)),p,q)) . q),((Swap ((id (dom T)),p,q)) . s)] by A1, Th65
.= [((Swap ((id (dom T)),p,q)) . q),((id (dom T)) . s)] by A3, Th33
.= [((Swap ((id (dom T)),p,q)) . q),s] by FUNCT_1:17
.= [((id (dom T)) . p),s] by A2, Th31
.= [p,s] by FUNCT_1:17 ; ::_thesis: verum
end;

Lm1:  for f being Function
for O being non empty connected Poset
for T being non empty array of O
for p, q being Element of dom T st p in q & f = (T,p,q) incl holds
for x1, x2, y1, y2 being Element of dom T st x1 in y1 & x2 in y2 & f . (x1,y1) = f . (x2,y2) holds
( x1 = x2 & y1 = y2 )
proof
let f be Function; ::_thesis: for O being non empty connected Poset
for T being non empty array of O
for p, q being Element of dom T st p in q & f = (T,p,q) incl holds
for x1, x2, y1, y2 being Element of dom T st x1 in y1 & x2 in y2 & f . (x1,y1) = f . (x2,y2) holds
( x1 = x2 & y1 = y2 )
let O be non empty connected Poset; ::_thesis: for T being non empty array of O
for p, q being Element of dom T st p in q & f = (T,p,q) incl holds
for x1, x2, y1, y2 being Element of dom T st x1 in y1 & x2 in y2 & f . (x1,y1) = f . (x2,y2) holds
( x1 = x2 & y1 = y2 )
let T be non empty array of O; ::_thesis: for p, q being Element of dom T st p in q & f = (T,p,q) incl holds
for x1, x2, y1, y2 being Element of dom T st x1 in y1 & x2 in y2 & f . (x1,y1) = f . (x2,y2) holds
( x1 = x2 & y1 = y2 )
let p, q be Element of dom T; ::_thesis: ( p in q & f = (T,p,q) incl implies for x1, x2, y1, y2 being Element of dom T st x1 in y1 & x2 in y2 & f . (x1,y1) = f . (x2,y2) holds
( x1 = x2 & y1 = y2 ) )
assume A1: ( p in q & f = (T,p,q) incl ) ; ::_thesis: for x1, x2, y1, y2 being Element of dom T st x1 in y1 & x2 in y2 & f . (x1,y1) = f . (x2,y2) holds
( x1 = x2 & y1 = y2 )
then A2: p <> q ;
let x1, x2, y1, y2 be Element of dom T; ::_thesis: ( x1 in y1 & x2 in y2 & f . (x1,y1) = f . (x2,y2) implies ( x1 = x2 & y1 = y2 ) )
assume that
A3: ( x1 in y1 & x2 in y2 ) and
A4: f . (x1,y1) = f . (x2,y2) ; ::_thesis: ( x1 = x2 & y1 = y2 )
set X = dom T;
set i = id (dom T);
set s = Swap ((id (dom T)),p,q);
set h = [:(Swap ((id (dom T)),p,q)),(Swap ((id (dom T)),p,q)):];
set Y = (succ q) \ p;
set Z1 = [:{p},((succ q) \ p):];
set Z2 = [:((succ q) \ p),{q}:];
set g = id ([:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:]);
percases ( ( x1 <> p & x1 <> q & y1 <> p & y1 <> q ) or ( x1 = p & y1 in q ) or ( x1 = p & y1 = q ) or ( p in x1 & y1 = q ) or ( x1 in p & y1 = p ) or ( x1 in p & y1 = q ) or ( x1 = p & q in y1 ) or ( x1 = q & q in y1 ) ) by A1, A3, Th2;
supposeA5: ( x1 <> p & x1 <> q & y1 <> p & y1 <> q ) ; ::_thesis: ( x1 = x2 & y1 = y2 )
then A6: f . (x1,y1) = [x1,y1] by A1, Th67;
percases ( S1[p,q,x2,y2] or S2[p,q,x2,y2] or S3[p,q,x2,y2] or S4[p,q,x2,y2] or S5[p,q,x2,y2] or S6[p,q,x2,y2] or S7[p,q,x2,y2] or S8[p,q,x2,y2] ) by A1, A3, Th2;
suppose S1[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  f . (x2,y2) = [x2,y2] by A1, Th67;
hence  ( x1 = x2 & y1 = y2 ) by A4, A6, XTUPLE_0:1; ::_thesis: verum
end;
suppose S2[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  f . (x2,y2) = [x2,q] by A1, Th68;
hence  ( x1 = x2 & y1 = y2 ) by A5, A4, A6, XTUPLE_0:1; ::_thesis: verum
end;
suppose S3[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  f . (x2,y2) = [x2,p] by A1, Th68;
hence  ( x1 = x2 & y1 = y2 ) by A5, A4, A6, XTUPLE_0:1; ::_thesis: verum
end;
suppose S4[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  f . (x2,y2) = [x2,y2] by A1, A3, Th69;
hence  ( x1 = x2 & y1 = y2 ) by A4, A6, XTUPLE_0:1; ::_thesis: verum
end;
suppose S5[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  f . (x2,y2) = [x2,y2] by A1, Th66;
hence  ( x1 = x2 & y1 = y2 ) by A4, A6, XTUPLE_0:1; ::_thesis: verum
end;
suppose S6[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  f . (x2,y2) = [q,y2] by A1, Th70;
hence  ( x1 = x2 & y1 = y2 ) by A5, A4, A6, XTUPLE_0:1; ::_thesis: verum
end;
suppose S7[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  f . (x2,y2) = [x2,y2] by A1, A3, Th69;
hence  ( x1 = x2 & y1 = y2 ) by A4, A6, XTUPLE_0:1; ::_thesis: verum
end;
suppose S8[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  f . (x2,y2) = [p,y2] by A1, Th70;
hence  ( x1 = x2 & y1 = y2 ) by A5, A4, A6, XTUPLE_0:1; ::_thesis: verum
end;
end;
end;
supposeA7: ( x1 = p & y1 in q ) ; ::_thesis: ( x1 = x2 & y1 = y2 )
then A8: f . (x1,y1) = [x1,y1] by A1, A3, Th69;
percases ( S1[p,q,x2,y2] or S2[p,q,x2,y2] or S3[p,q,x2,y2] or S4[p,q,x2,y2] or S5[p,q,x2,y2] or S6[p,q,x2,y2] or S7[p,q,x2,y2] or S8[p,q,x2,y2] ) by A1, A3, Th2;
suppose S1[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  f . (x2,y2) = [x2,y2] by A1, Th67;
hence  ( x1 = x2 & y1 = y2 ) by A4, A8, XTUPLE_0:1; ::_thesis: verum
end;
suppose S2[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  ( f . (x2,y2) = [x2,q] & x2 <> p ) by A1, Th68;
hence  ( x1 = x2 & y1 = y2 ) by A7, A4, A8, XTUPLE_0:1; ::_thesis: verum
end;
suppose S3[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  ( f . (x2,y2) = [x2,p] & x2 <> p ) by A1, Th68;
hence  ( x1 = x2 & y1 = y2 ) by A7, A4, A8, XTUPLE_0:1; ::_thesis: verum
end;
suppose S4[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  f . (x2,y2) = [x2,y2] by A1, A3, Th69;
hence  ( x1 = x2 & y1 = y2 ) by A4, A8, XTUPLE_0:1; ::_thesis: verum
end;
suppose S5[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  f . (x2,y2) = [x2,y2] by A1, Th66;
hence  ( x1 = x2 & y1 = y2 ) by A4, A8, XTUPLE_0:1; ::_thesis: verum
end;
suppose S6[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  f . (x2,y2) = [q,y2] by A1, Th70;
hence  ( x1 = x2 & y1 = y2 ) by A2, A7, A4, A8, XTUPLE_0:1; ::_thesis: verum
end;
suppose S7[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  f . (x2,y2) = [x2,y2] by A1, A3, Th69;
hence  ( x1 = x2 & y1 = y2 ) by A4, A8, XTUPLE_0:1; ::_thesis: verum
end;
supposeA9: S8[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  f . (x2,y2) = [p,y2] by A1, Th70;
hence  ( x1 = x2 & y1 = y2 ) by A7, A9, A4, A8, XTUPLE_0:1; ::_thesis: verum
end;
end;
end;
supposeA10: ( x1 = p & y1 = q ) ; ::_thesis: ( x1 = x2 & y1 = y2 )
then A11: f . (x1,y1) = [x1,y1] by A1, Th66;
percases ( S1[p,q,x2,y2] or S2[p,q,x2,y2] or S3[p,q,x2,y2] or S4[p,q,x2,y2] or S5[p,q,x2,y2] or S6[p,q,x2,y2] or S7[p,q,x2,y2] or S8[p,q,x2,y2] ) by A1, A3, Th2;
suppose S1[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  f . (x2,y2) = [x2,y2] by A1, Th67;
hence  ( x1 = x2 & y1 = y2 ) by A4, A11, XTUPLE_0:1; ::_thesis: verum
end;
suppose S2[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  ( f . (x2,y2) = [x2,q] & x2 <> p ) by A1, Th68;
hence  ( x1 = x2 & y1 = y2 ) by A10, A4, A11, XTUPLE_0:1; ::_thesis: verum
end;
suppose S3[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  f . (x2,y2) = [x2,p] by A1, Th68;
hence  ( x1 = x2 & y1 = y2 ) by A2, A10, A4, A11, XTUPLE_0:1; ::_thesis: verum
end;
suppose S4[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  f . (x2,y2) = [x2,y2] by A1, A3, Th69;
hence  ( x1 = x2 & y1 = y2 ) by A4, A11, XTUPLE_0:1; ::_thesis: verum
end;
suppose S5[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  f . (x2,y2) = [x2,y2] by A1, Th66;
hence  ( x1 = x2 & y1 = y2 ) by A4, A11, XTUPLE_0:1; ::_thesis: verum
end;
suppose S6[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  f . (x2,y2) = [q,y2] by A1, Th70;
hence  ( x1 = x2 & y1 = y2 ) by A2, A10, A4, A11, XTUPLE_0:1; ::_thesis: verum
end;
suppose S7[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  f . (x2,y2) = [x2,y2] by A1, A3, Th69;
hence  ( x1 = x2 & y1 = y2 ) by A4, A11, XTUPLE_0:1; ::_thesis: verum
end;
suppose S8[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  ( f . (x2,y2) = [p,y2] & y2 <> q ) by A1, Th70;
hence  ( x1 = x2 & y1 = y2 ) by A10, A4, A11, XTUPLE_0:1; ::_thesis: verum
end;
end;
end;
supposeA12: ( p in x1 & y1 = q ) ; ::_thesis: ( x1 = x2 & y1 = y2 )
then A13: f . (x1,y1) = [x1,y1] by A1, A3, Th69;
percases ( S1[p,q,x2,y2] or S2[p,q,x2,y2] or S3[p,q,x2,y2] or S4[p,q,x2,y2] or S5[p,q,x2,y2] or S6[p,q,x2,y2] or S7[p,q,x2,y2] or S8[p,q,x2,y2] ) by A1, A3, Th2;
suppose S1[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  f . (x2,y2) = [x2,y2] by A1, Th67;
hence  ( x1 = x2 & y1 = y2 ) by A4, A13, XTUPLE_0:1; ::_thesis: verum
end;
supposeA14: S2[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  f . (x2,y2) = [x2,q] by A1, Th68;
hence  ( x1 = x2 & y1 = y2 ) by A14, A12, A4, A13, XTUPLE_0:1; ::_thesis: verum
end;
supposeA15: S3[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  f . (x2,y2) = [x2,p] by A1, Th68;
hence  ( x1 = x2 & y1 = y2 ) by A15, A12, A4, A13, XTUPLE_0:1; ::_thesis: verum
end;
suppose S4[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  f . (x2,y2) = [x2,y2] by A1, A3, Th69;
hence  ( x1 = x2 & y1 = y2 ) by A4, A13, XTUPLE_0:1; ::_thesis: verum
end;
suppose S5[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  f . (x2,y2) = [x2,y2] by A1, Th66;
hence  ( x1 = x2 & y1 = y2 ) by A4, A13, XTUPLE_0:1; ::_thesis: verum
end;
suppose S6[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  ( f . (x2,y2) = [q,y2] & y2 <> q ) by A1, Th70;
hence  ( x1 = x2 & y1 = y2 ) by A12, A4, A13, XTUPLE_0:1; ::_thesis: verum
end;
suppose S7[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  f . (x2,y2) = [x2,y2] by A1, A3, Th69;
hence  ( x1 = x2 & y1 = y2 ) by A4, A13, XTUPLE_0:1; ::_thesis: verum
end;
suppose S8[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  ( f . (x2,y2) = [p,y2] & y2 <> q ) by A1, Th70;
hence  ( x1 = x2 & y1 = y2 ) by A12, A4, A13, XTUPLE_0:1; ::_thesis: verum
end;
end;
end;
supposeA16: ( x1 in p & y1 = p ) ; ::_thesis: ( x1 = x2 & y1 = y2 )
then A17: f . (x1,y1) = [x1,q] by A1, Th68;
percases ( S1[p,q,x2,y2] or S2[p,q,x2,y2] or S3[p,q,x2,y2] or S4[p,q,x2,y2] or S5[p,q,x2,y2] or S6[p,q,x2,y2] or S7[p,q,x2,y2] or S8[p,q,x2,y2] ) by A1, A3, Th2;
supposeA18: S1[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  f . (x2,y2) = [x2,y2] by A1, Th67;
hence  ( x1 = x2 & y1 = y2 ) by A18, A4, A17, XTUPLE_0:1; ::_thesis: verum
end;
supposeA19: S2[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  f . (x2,y2) = [x2,q] by A1, Th68;
hence  ( x1 = x2 & y1 = y2 ) by A19, A16, A4, A17, XTUPLE_0:1; ::_thesis: verum
end;
suppose S3[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  f . (x2,y2) = [x2,p] by A1, Th68;
hence  ( x1 = x2 & y1 = y2 ) by A2, A4, A17, XTUPLE_0:1; ::_thesis: verum
end;
suppose S4[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  ( f . (x2,y2) = [x2,y2] & x2 <> x1 ) by A16, A1, A3, Th69;
hence  ( x1 = x2 & y1 = y2 ) by A4, A17, XTUPLE_0:1; ::_thesis: verum
end;
suppose S5[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  ( f . (x2,y2) = [x2,y2] & x2 <> x1 ) by A16, A1, Th66;
hence  ( x1 = x2 & y1 = y2 ) by A4, A17, XTUPLE_0:1; ::_thesis: verum
end;
suppose S6[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  ( f . (x2,y2) = [q,y2] & y2 <> q ) by A1, Th70;
hence  ( x1 = x2 & y1 = y2 ) by A4, A17, XTUPLE_0:1; ::_thesis: verum
end;
supposeA20: S7[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  f . (x2,y2) = [x2,y2] by A1, A3, Th69;
hence  ( x1 = x2 & y1 = y2 ) by A16, A20, A4, A17, XTUPLE_0:1; ::_thesis: verum
end;
suppose S8[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  ( f . (x2,y2) = [p,y2] & x1 <> p ) by A16, A1, Th70;
hence  ( x1 = x2 & y1 = y2 ) by A4, A17, XTUPLE_0:1; ::_thesis: verum
end;
end;
end;
supposeA21: ( x1 in p & y1 = q ) ; ::_thesis: ( x1 = x2 & y1 = y2 )
then A22: f . (x1,y1) = [x1,p] by A1, Th68;
percases ( S1[p,q,x2,y2] or S2[p,q,x2,y2] or S3[p,q,x2,y2] or S4[p,q,x2,y2] or S5[p,q,x2,y2] or S6[p,q,x2,y2] or S7[p,q,x2,y2] or S8[p,q,x2,y2] ) by A1, A3, Th2;
supposeA23: S1[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  f . (x2,y2) = [x2,y2] by A1, Th67;
hence  ( x1 = x2 & y1 = y2 ) by A23, A4, A22, XTUPLE_0:1; ::_thesis: verum
end;
suppose S2[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  f . (x2,y2) = [x2,q] by A1, Th68;
hence  ( x1 = x2 & y1 = y2 ) by A2, A4, A22, XTUPLE_0:1; ::_thesis: verum
end;
supposeA24: S3[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  f . (x2,y2) = [x2,p] by A1, Th68;
hence  ( x1 = x2 & y1 = y2 ) by A24, A21, A4, A22, XTUPLE_0:1; ::_thesis: verum
end;
supposeA25: S4[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  ( f . (x2,y2) = [x2,y2] & x1 <> p ) by A21, A1, A3, Th69;
hence  ( x1 = x2 & y1 = y2 ) by A25, A4, A22, XTUPLE_0:1; ::_thesis: verum
end;
supposeA26: S5[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  f . (x2,y2) = [x2,y2] by A1, Th66;
hence  ( x1 = x2 & y1 = y2 ) by A26, A2, A4, A22, XTUPLE_0:1; ::_thesis: verum
end;
suppose S6[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  f . (x2,y2) = [q,y2] by A1, Th70;
hence  ( x1 = x2 & y1 = y2 ) by A1, A21, A4, A22, XTUPLE_0:1; ::_thesis: verum
end;
supposeA27: S7[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  f . (x2,y2) = [x2,y2] by A1, A3, Th69;
hence  ( x1 = x2 & y1 = y2 ) by A2, A27, A4, A22, XTUPLE_0:1; ::_thesis: verum
end;
suppose S8[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  ( f . (x2,y2) = [p,y2] & x1 <> p ) by A21, A1, Th70;
hence  ( x1 = x2 & y1 = y2 ) by A4, A22, XTUPLE_0:1; ::_thesis: verum
end;
end;
end;
supposeA28: ( x1 = p & q in y1 ) ; ::_thesis: ( x1 = x2 & y1 = y2 )
then A29: f . (x1,y1) = [q,y1] by A1, Th70;
percases ( S1[p,q,x2,y2] or S2[p,q,x2,y2] or S3[p,q,x2,y2] or S4[p,q,x2,y2] or S5[p,q,x2,y2] or S6[p,q,x2,y2] or S7[p,q,x2,y2] or S8[p,q,x2,y2] ) by A1, A3, Th2;
supposeA30: S1[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  f . (x2,y2) = [x2,y2] by A1, Th67;
hence  ( x1 = x2 & y1 = y2 ) by A30, A4, A29, XTUPLE_0:1; ::_thesis: verum
end;
supposeA31: S2[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  f . (x2,y2) = [x2,q] by A1, Th68;
hence  ( x1 = x2 & y1 = y2 ) by A1, A31, A4, A29, XTUPLE_0:1; ::_thesis: verum
end;
suppose S3[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  f . (x2,y2) = [x2,p] by A1, Th68;
hence  ( x1 = x2 & y1 = y2 ) by A1, A28, A4, A29, XTUPLE_0:1; ::_thesis: verum
end;
suppose S4[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  ( f . (x2,y2) = [x2,y2] & x2 <> q ) by A1, A3, Th69;
hence  ( x1 = x2 & y1 = y2 ) by A4, A29, XTUPLE_0:1; ::_thesis: verum
end;
supposeA32: S5[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  f . (x2,y2) = [x2,y2] by A1, Th66;
hence  ( x1 = x2 & y1 = y2 ) by A2, A32, A4, A29, XTUPLE_0:1; ::_thesis: verum
end;
supposeA33: S6[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  f . (x2,y2) = [q,y2] by A1, Th70;
hence  ( x1 = x2 & y1 = y2 ) by A33, A28, A4, A29, XTUPLE_0:1; ::_thesis: verum
end;
suppose S7[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  ( f . (x2,y2) = [x2,y2] & x2 <> q ) by A1, A3, Th69;
hence  ( x1 = x2 & y1 = y2 ) by A4, A29, XTUPLE_0:1; ::_thesis: verum
end;
suppose S8[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  f . (x2,y2) = [p,y2] by A1, Th70;
hence  ( x1 = x2 & y1 = y2 ) by A2, A4, A29, XTUPLE_0:1; ::_thesis: verum
end;
end;
end;
supposeA34: ( x1 = q & q in y1 ) ; ::_thesis: ( x1 = x2 & y1 = y2 )
then A35: f . (x1,y1) = [p,y1] by A1, Th70;
percases ( S1[p,q,x2,y2] or S2[p,q,x2,y2] or S3[p,q,x2,y2] or S4[p,q,x2,y2] or S5[p,q,x2,y2] or S6[p,q,x2,y2] or S7[p,q,x2,y2] or S8[p,q,x2,y2] ) by A1, A3, Th2;
supposeA36: S1[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  f . (x2,y2) = [x2,y2] by A1, Th67;
hence  ( x1 = x2 & y1 = y2 ) by A36, A4, A35, XTUPLE_0:1; ::_thesis: verum
end;
suppose S2[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  ( f . (x2,y2) = [x2,q] & p <> x2 ) by A1, Th68;
hence  ( x1 = x2 & y1 = y2 ) by A4, A35, XTUPLE_0:1; ::_thesis: verum
end;
suppose S3[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  ( f . (x2,y2) = [x2,p] & p <> x2 ) by A1, Th68;
hence  ( x1 = x2 & y1 = y2 ) by A4, A35, XTUPLE_0:1; ::_thesis: verum
end;
supposeA37: S4[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  f . (x2,y2) = [x2,y2] by A1, A3, Th69;
hence  ( x1 = x2 & y1 = y2 ) by A34, A37, A4, A35, XTUPLE_0:1; ::_thesis: verum
end;
suppose S5[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  ( f . (x2,y2) = [x2,y2] & y1 <> y2 ) by A34, A1, Th66;
hence  ( x1 = x2 & y1 = y2 ) by A4, A35, XTUPLE_0:1; ::_thesis: verum
end;
suppose S6[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  f . (x2,y2) = [q,y2] by A1, Th70;
hence  ( x1 = x2 & y1 = y2 ) by A2, A4, A35, XTUPLE_0:1; ::_thesis: verum
end;
suppose S7[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  ( f . (x2,y2) = [x2,y2] & y2 <> y1 ) by A34, A1, A3, Th69;
hence  ( x1 = x2 & y1 = y2 ) by A4, A35, XTUPLE_0:1; ::_thesis: verum
end;
supposeA38: S8[p,q,x2,y2] ; ::_thesis: ( x1 = x2 & y1 = y2 )
then  f . (x2,y2) = [p,y2] by A1, Th70;
hence  ( x1 = x2 & y1 = y2 ) by A38, A34, A4, A35, XTUPLE_0:1; ::_thesis: verum
end;
end;
end;
end;
end;

theorem Th71: :: EXCHSORT:71
for O being non empty connected Poset
for T being non empty array of O
for p, q being Element of dom T st p in q holds
((T,p,q) incl) | (inversions (Swap (T,p,q))) is one-to-one
proof
let O be non empty connected Poset; ::_thesis: for T being non empty array of O
for p, q being Element of dom T st p in q holds
((T,p,q) incl) | (inversions (Swap (T,p,q))) is one-to-one
let T be non empty array of O; ::_thesis: for p, q being Element of dom T st p in q holds
((T,p,q) incl) | (inversions (Swap (T,p,q))) is one-to-one
let p, q be Element of dom T; ::_thesis: ( p in q implies ((T,p,q) incl) | (inversions (Swap (T,p,q))) is one-to-one )
assume A1: p in q ; ::_thesis: ((T,p,q) incl) | (inversions (Swap (T,p,q))) is one-to-one
set f = (T,p,q) incl ;
set s = Swap (T,p,q);
set w = inversions (Swap (T,p,q));
set fw = ((T,p,q) incl) | (inversions (Swap (T,p,q)));
A2: dom (Swap (T,p,q)) = dom T by FUNCT_7:99;
let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not x in proj1 (((T,p,q) incl) | (inversions (Swap (T,p,q)))) or not b1 in proj1 (((T,p,q) incl) | (inversions (Swap (T,p,q)))) or not (((T,p,q) incl) | (inversions (Swap (T,p,q)))) . x = (((T,p,q) incl) | (inversions (Swap (T,p,q)))) . b1 or x = b1 )
let y be set ; ::_thesis: ( not x in proj1 (((T,p,q) incl) | (inversions (Swap (T,p,q)))) or not y in proj1 (((T,p,q) incl) | (inversions (Swap (T,p,q)))) or not (((T,p,q) incl) | (inversions (Swap (T,p,q)))) . x = (((T,p,q) incl) | (inversions (Swap (T,p,q)))) . y or x = y )
assume  ( x in dom (((T,p,q) incl) | (inversions (Swap (T,p,q)))) & y in dom (((T,p,q) incl) | (inversions (Swap (T,p,q)))) ) ; ::_thesis: ( not (((T,p,q) incl) | (inversions (Swap (T,p,q)))) . x = (((T,p,q) incl) | (inversions (Swap (T,p,q)))) . y or x = y )
then A3: ( x in inversions (Swap (T,p,q)) & y in inversions (Swap (T,p,q)) ) by RELAT_1:57;
then consider x1, y1 being Element of dom T such that
A4: ( x = [x1,y1] & x1 in y1 & (Swap (T,p,q)) /. x1 > (Swap (T,p,q)) /. y1 ) by A2;
consider x2, y2 being Element of dom T such that
A5: ( y = [x2,y2] & x2 in y2 & (Swap (T,p,q)) /. x2 > (Swap (T,p,q)) /. y2 ) by A2, A3;
assume  (((T,p,q) incl) | (inversions (Swap (T,p,q)))) . x = (((T,p,q) incl) | (inversions (Swap (T,p,q)))) . y ; ::_thesis: x = y
then ((T,p,q) incl) . (x1,y1) = (((T,p,q) incl) | (inversions (Swap (T,p,q)))) . y by A4, A3, FUNCT_1:49
.= ((T,p,q) incl) . (x2,y2) by A5, A3, FUNCT_1:49 ;
then  ( x1 = x2 & y1 = y2 ) by A1, A4, A5, Lm1;
hence  x = y by A4, A5; ::_thesis: verum
end;

registration
let O be non empty connected Poset;
let R be array of O;
let x, y, z be set ;
cluster((R,x,y) incl) .: z ->  Relation-like ;
coherence
 ((R,x,y) incl) .: z is Relation-like
proof
set X = dom R;
set i = id (dom R);
set s = Swap ((id (dom R)),x,y);
set h = [:(Swap ((id (dom R)),x,y)),(Swap ((id (dom R)),x,y)):];
set Y = (succ y) \ x;
set Z1 = [:{x},((succ y) \ x):];
set Z2 = [:((succ y) \ x),{y}:];
set g = id ([:{x},((succ y) \ x):] \/ [:((succ y) \ x),{y}:]);
A1: ((R,x,y) incl) .: z c= rng ((R,x,y) incl) by RELAT_1:111;
A2: rng [:(Swap ((id (dom R)),x,y)),(Swap ((id (dom R)),x,y)):] = [:(rng (Swap ((id (dom R)),x,y))),(rng (Swap ((id (dom R)),x,y))):] by FUNCT_3:67;
 rng ((R,x,y) incl) c= (rng [:(Swap ((id (dom R)),x,y)),(Swap ((id (dom R)),x,y)):]) \/ (rng (id ([:{x},((succ y) \ x):] \/ [:((succ y) \ x),{y}:]))) by FUNCT_4:17;
hence  ((R,x,y) incl) .: z is Relation-like by A1, A2; ::_thesis: verum
end;
end;

begin

theorem Th72: :: EXCHSORT:72
for x, y being set
for O being non empty connected Poset
for R being array of O st [x,y] in inversions R holds
((R,x,y) incl) .: (inversions (Swap (R,x,y))) c< inversions R
proof
let x, y be set ; ::_thesis: for O being non empty connected Poset
for R being array of O st [x,y] in inversions R holds
((R,x,y) incl) .: (inversions (Swap (R,x,y))) c< inversions R
let O be non empty connected Poset; ::_thesis: for R being array of O st [x,y] in inversions R holds
((R,x,y) incl) .: (inversions (Swap (R,x,y))) c< inversions R
let R be array of O; ::_thesis: ( [x,y] in inversions R implies ((R,x,y) incl) .: (inversions (Swap (R,x,y))) c< inversions R )
assume A1: [x,y] in inversions R ; ::_thesis: ((R,x,y) incl) .: (inversions (Swap (R,x,y))) c< inversions R
then A2: ( x in dom R & y in dom R & x in y & R /. x > R /. y ) by Th46;
reconsider T = R as non empty array of O by A1;
reconsider p = x, q = y as Element of dom T by A1, Th46;
set j = (R,x,y) incl ;
set k = (T,p,q) incl ;
set s = Swap (R,x,y);
set t = Swap (T,p,q);
set ws = inversions (Swap (R,x,y));
set w = inversions R;
A3: dom (Swap (T,p,q)) = dom T by FUNCT_7:99;
thus  ((R,x,y) incl) .: (inversions (Swap (R,x,y))) c= inversions R :: according to XBOOLE_0:def_8 ::_thesis: not ((R,x,y) incl) .: (inversions (Swap (R,x,y))) = inversions R
proof
let z be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds
( not [z,b1] in ((R,x,y) incl) .: (inversions (Swap (R,x,y))) or [z,b1] in inversions R )
let t be set ; ::_thesis: ( not [z,t] in ((R,x,y) incl) .: (inversions (Swap (R,x,y))) or [z,t] in inversions R )
assume  [z,t] in ((R,x,y) incl) .: (inversions (Swap (R,x,y))) ; ::_thesis: [z,t] in inversions R
then consider a, b being set  such that
A4: ( [a,b] in inversions (Swap (R,x,y)) & [a,b] in dom ((R,x,y) incl) & [z,t] = ((R,x,y) incl) . (a,b) ) by Th5;
A5: ( a in b & a in dom T & b in dom T ) by A4, A3, Th46;
reconsider a = a, b = b as Element of dom T by A4, A3, Th46;
percases ( ( a <> p & a <> q & b <> p & b <> q ) or ( a in p & b = p ) or ( a in p & b = q ) or ( a = p & b in q ) or ( a = p & b = q ) or ( a = p & q in b ) or ( a = q & q in b ) or ( p in a & q = b ) ) by A2, A5, Th2;
supposeA6: ( a <> p & a <> q & b <> p & b <> q ) ; ::_thesis: [z,t] in inversions R
then  [z,t] = [a,b] by A4, A2, Th67;
hence  [z,t] in inversions R by A4, A6, Th52; ::_thesis: verum
end;
supposeA7: ( a in p & b = p ) ; ::_thesis: [z,t] in inversions R
then  [z,t] = [a,q] by A4, A2, Th68;
hence  [z,t] in inversions R by A1, A4, A7, Th53; ::_thesis: verum
end;
supposeA8: ( a in p & b = q ) ; ::_thesis: [z,t] in inversions R
then  [z,t] = [a,p] by A4, A2, Th68;
hence  [z,t] in inversions R by A1, A4, A8, Th54; ::_thesis: verum
end;
supposeA9: ( a = p & b in q ) ; ::_thesis: [z,t] in inversions R
then  [z,t] = [a,b] by A5, A4, Th69;
hence  [z,t] in inversions R by A1, A4, A9, Th55; ::_thesis: verum
end;
suppose ( a = p & b = q ) ; ::_thesis: [z,t] in inversions R
hence  [z,t] in inversions R by A1, A4, A2, Th66; ::_thesis: verum
end;
supposeA10: ( a = p & q in b ) ; ::_thesis: [z,t] in inversions R
then  [z,t] = [q,b] by A4, A2, Th70;
hence  [z,t] in inversions R by A1, A4, A10, Th57; ::_thesis: verum
end;
supposeA11: ( a = q & q in b ) ; ::_thesis: [z,t] in inversions R
then  [z,t] = [p,b] by A4, A2, Th70;
hence  [z,t] in inversions R by A1, A4, A11, Th58; ::_thesis: verum
end;
supposeA12: ( p in a & q = b ) ; ::_thesis: [z,t] in inversions R
then  [z,t] = [a,b] by A4, A5, Th69;
hence  [z,t] in inversions R by A1, A4, A12, Th56; ::_thesis: verum
end;
end;
end;
now__::_thesis:_(_[x,y]_in_((R,x,y)_incl)_.:_(inversions_(Swap_(R,x,y)))_implies_[x,y]_in_inversions_(Swap_(R,x,y))_)
assume  [x,y] in ((R,x,y) incl) .: (inversions (Swap (R,x,y))) ; ::_thesis: [x,y] in inversions (Swap (R,x,y))
then consider a, b being set  such that
A13: ( [a,b] in inversions (Swap (R,x,y)) & [a,b] in dom ((R,x,y) incl) & [x,y] = ((R,x,y) incl) . (a,b) ) by Th5;
A14: ((R,x,y) incl) . (p,q) = [p,q] by A2, Th66;
A15: ( a in b & a in dom T & b in dom T ) by A13, A3, Th46;
reconsider a = a, b = b as Element of dom T by A13, A3, Th46;
 ( a = p & b = q ) by A2, A13, A14, A15, Lm1;
hence  [x,y] in inversions (Swap (R,x,y)) by A13; ::_thesis: verum
end;
hence  not ((R,x,y) incl) .: (inversions (Swap (R,x,y))) = inversions R by A1, Th51; ::_thesis: verum
end;

registration
let R be finite Function;
let x, y be set ;
cluster Swap (R,x,y) ->  finite ;
coherence
 Swap (R,x,y) is finite
proof
 dom (Swap (R,x,y)) = dom R by FUNCT_7:99;
hence  Swap (R,x,y) is finite by FINSET_1:10; ::_thesis: verum
end;
end;

theorem Th73: :: EXCHSORT:73
for x, y being set
for O being non empty connected Poset
for R being array of O st [x,y] in inversions R & inversions R is finite holds
card (inversions (Swap (R,x,y))) in card (inversions R)
proof
let x, y be set ; ::_thesis: for O being non empty connected Poset
for R being array of O st [x,y] in inversions R & inversions R is finite holds
card (inversions (Swap (R,x,y))) in card (inversions R)
let O be non empty connected Poset; ::_thesis: for R being array of O st [x,y] in inversions R & inversions R is finite holds
card (inversions (Swap (R,x,y))) in card (inversions R)
let R be array of O; ::_thesis: ( [x,y] in inversions R & inversions R is finite implies card (inversions (Swap (R,x,y))) in card (inversions R) )
set s = Swap (R,x,y);
set h = (R,x,y) incl ;
set ws = inversions (Swap (R,x,y));
assume A1: ( [x,y] in inversions R & inversions R is finite ) ; ::_thesis: card (inversions (Swap (R,x,y))) in card (inversions R)
then reconsider w = inversions R as finite set ;
 ((R,x,y) incl) .: (inversions (Swap (R,x,y))) c< inversions R by A1, Th72;
then  ((R,x,y) incl) .: (inversions (Swap (R,x,y))) c= w by XBOOLE_0:def_8;
then reconsider hws = ((R,x,y) incl) .: (inversions (Swap (R,x,y))) as finite set ;
 card hws < card w by A1, Th72, TREES_1:6;
then A2: card hws in card w by NAT_1:44;
A3: ( x in dom R & y in dom R & x in y ) by A1, Th46;
A4: not R is empty by A1;
 inversions (Swap (R,x,y)),((R,x,y) incl) .: (inversions (Swap (R,x,y))) are_equipotent
proof
take hw = ((R,x,y) incl) | (inversions (Swap (R,x,y))); :: according to WELLORD2:def_4 ::_thesis: ( hw is one-to-one & proj1 hw = inversions (Swap (R,x,y)) & proj2 hw = ((R,x,y) incl) .: (inversions (Swap (R,x,y))) )
thus  hw is one-to-one by A3, A4, Th71; ::_thesis: ( proj1 hw = inversions (Swap (R,x,y)) & proj2 hw = ((R,x,y) incl) .: (inversions (Swap (R,x,y))) )
 dom (Swap (R,x,y)) = dom R by FUNCT_7:99;
then  inversions (Swap (R,x,y)) c= [:(dom R),(dom R):] by Th47;
then  inversions (Swap (R,x,y)) c= dom ((R,x,y) incl) by A3, A4, Th61;
hence  dom hw = inversions (Swap (R,x,y)) by RELAT_1:62; ::_thesis: proj2 hw = ((R,x,y) incl) .: (inversions (Swap (R,x,y)))
thus  proj2 hw = ((R,x,y) incl) .: (inversions (Swap (R,x,y))) by RELAT_1:115; ::_thesis: verum
end;
hence  card (inversions (Swap (R,x,y))) in card (inversions R) by A2, CARD_1:5; ::_thesis: verum
end;

theorem :: EXCHSORT:74
for x, y being set
for O being non empty connected Poset
for R being finite array of O st [x,y] in inversions R holds
card (inversions (Swap (R,x,y))) < card (inversions R)
proof
let x, y be set ; ::_thesis: for O being non empty connected Poset
for R being finite array of O st [x,y] in inversions R holds
card (inversions (Swap (R,x,y))) < card (inversions R)
let O be non empty connected Poset; ::_thesis: for R being finite array of O st [x,y] in inversions R holds
card (inversions (Swap (R,x,y))) < card (inversions R)
let R be finite array of O; ::_thesis: ( [x,y] in inversions R implies card (inversions (Swap (R,x,y))) < card (inversions R) )
assume  [x,y] in inversions R ; ::_thesis: card (inversions (Swap (R,x,y))) < card (inversions R)
then  card (inversions (Swap (R,x,y))) in card (inversions R) by Th73;
hence  card (inversions (Swap (R,x,y))) < card (inversions R) by NAT_1:44; ::_thesis: verum
end;

definition
let O be non empty connected Poset;
let R be array of O;
mode arr_computation of R ->  non empty array means :Def14: :: EXCHSORT:def 14
( it . (base- it) = R & ( for a being ordinal number st a in dom it holds
it . a is array of O ) & ( for a being ordinal number st a in dom it & succ a in dom it holds
ex R being array of O ex x, y being set st
( [x,y] in inversions R & it . a = R & it . (succ a) = Swap (R,x,y) ) ) );
existence
 ex b1 being non empty array st
( b1 . (base- b1) = R & ( for a being ordinal number st a in dom b1 holds
b1 . a is array of O ) & ( for a being ordinal number st a in dom b1 & succ a in dom b1 holds
ex R being array of O ex x, y being set st
( [x,y] in inversions R & b1 . a = R & b1 . (succ a) = Swap (R,x,y) ) ) )
proof
reconsider C = <%R%> as non empty 0 -based array ;
take  C ; ::_thesis: ( C . (base- C) = R & ( for a being ordinal number st a in dom C holds
C . a is array of O ) & ( for a being ordinal number st a in dom C & succ a in dom C holds
ex R being array of O ex x, y being set st
( [x,y] in inversions R & C . a = R & C . (succ a) = Swap (R,x,y) ) ) )
A1: ( dom C = 1 & 0 in 1 ) by AFINSQ_1:def_4, NAT_1:44;
then  base- C = 0 by Def4;
hence  C . (base- C) = R by AFINSQ_1:def_4; ::_thesis: ( ( for a being ordinal number st a in dom C holds
C . a is array of O ) & ( for a being ordinal number st a in dom C & succ a in dom C holds
ex R being array of O ex x, y being set st
( [x,y] in inversions R & C . a = R & C . (succ a) = Swap (R,x,y) ) ) )
hereby  ::_thesis: for a being ordinal number st a in dom C & succ a in dom C holds
ex R being array of O ex x, y being set st
( [x,y] in inversions R & C . a = R & C . (succ a) = Swap (R,x,y) )
let a be ordinal number ; ::_thesis: ( a in dom C implies C . a is array of O )
assume  a in dom C ; ::_thesis: C . a is array of O
then  a = 0 by A1, ORDINAL3:15, TARSKI:def_1;
hence  C . a is array of O by AFINSQ_1:def_4; ::_thesis: verum
end;
let a be ordinal number ; ::_thesis: ( a in dom C & succ a in dom C implies ex R being array of O ex x, y being set st
( [x,y] in inversions R & C . a = R & C . (succ a) = Swap (R,x,y) ) )
assume  ( a in dom C & succ a in dom C ) ; ::_thesis: ex R being array of O ex x, y being set st
( [x,y] in inversions R & C . a = R & C . (succ a) = Swap (R,x,y) )
hence  ex R being array of O ex x, y being set st
( [x,y] in inversions R & C . a = R & C . (succ a) = Swap (R,x,y) ) by A1, ORDINAL3:15, TARSKI:def_1; ::_thesis: verum
end;
end;

:: deftheorem Def14 defines arr_computation EXCHSORT:def_14_:_
 for O being non empty connected Poset
for R being array of O
for b3 being non empty array holds
( b3 is arr_computation of R iff ( b3 . (base- b3) = R & ( for a being ordinal number st a in dom b3 holds
b3 . a is array of O ) & ( for a being ordinal number st a in dom b3 & succ a in dom b3 holds
ex R being array of O ex x, y being set st
( [x,y] in inversions R & b3 . a = R & b3 . (succ a) = Swap (R,x,y) ) ) ) );

theorem Th75: :: EXCHSORT:75
for a being ordinal number
for O being non empty connected Poset
for R being array of O holds {[a,R]} is arr_computation of R
proof
let a be ordinal number ; ::_thesis: for O being non empty connected Poset
for R being array of O holds {[a,R]} is arr_computation of R
let O be non empty connected Poset; ::_thesis: for R being array of O holds {[a,R]} is arr_computation of R
let R be array of O; ::_thesis: {[a,R]} is arr_computation of R
reconsider C = {[a,R]} as non empty a -based array ;
 C is arr_computation of R
proof
A1: ( dom C = {a} & a in {a} ) by FUNCT_5:12, TARSKI:def_1;
then  base- C = a by Def4;
hence  C . (base- C) = R by GRFUNC_1:6; :: according to EXCHSORT:def_14 ::_thesis: ( ( for a being ordinal number st a in dom C holds
C . a is array of O ) & ( for a being ordinal number st a in dom C & succ a in dom C holds
ex R being array of O ex x, y being set st
( [x,y] in inversions R & C . a = R & C . (succ a) = Swap (R,x,y) ) ) )
hereby  ::_thesis: for a being ordinal number st a in dom C & succ a in dom C holds
ex R being array of O ex x, y being set st
( [x,y] in inversions R & C . a = R & C . (succ a) = Swap (R,x,y) )
let b be ordinal number ; ::_thesis: ( b in dom C implies C . b is array of O )
assume  b in dom C ; ::_thesis: C . b is array of O
then  a = b by A1, TARSKI:def_1;
hence  C . b is array of O by GRFUNC_1:6; ::_thesis: verum
end;
let b be ordinal number ; ::_thesis: ( b in dom C & succ b in dom C implies ex R being array of O ex x, y being set st
( [x,y] in inversions R & C . b = R & C . (succ b) = Swap (R,x,y) ) )
assume  ( b in dom C & succ b in dom C ) ; ::_thesis: ex R being array of O ex x, y being set st
( [x,y] in inversions R & C . b = R & C . (succ b) = Swap (R,x,y) )
then  ( a = b & a = succ b ) by A1, TARSKI:def_1;
then  a in a by ORDINAL1:6;
hence  ex R being array of O ex x, y being set st
( [x,y] in inversions R & C . b = R & C . (succ b) = Swap (R,x,y) ) ; ::_thesis: verum
end;
hence  {[a,R]} is arr_computation of R ; ::_thesis: verum
end;

registration
let O be non empty connected Poset;
let R be array of O;
let a be ordinal number ;
cluster non empty Relation-like Function-like finite segmental a -based for arr_computation of R;
existence
 ex b1 being arr_computation of R st
( b1 is a -based & b1 is finite )
proof
reconsider C = {[a,R]} as non empty finite a -based array ;
 C is arr_computation of R by Th75;
hence  ex b1 being arr_computation of R st
( b1 is a -based & b1 is finite ) ; ::_thesis: verum
end;
end;

registration
let O be non empty connected Poset;
let R be array of O;
let C be arr_computation of R;
let x be set ;
clusterC . x ->  Relation-like Function-like segmental ;
coherence
 ( C . x is segmental & C . x is Function-like & C . x is Relation-like )
proof
percases ( x nin dom C or x in dom C ) ;
suppose x nin dom C ; ::_thesis: ( C . x is segmental & C . x is Function-like & C . x is Relation-like )
hence  ( C . x is segmental & C . x is Function-like & C . x is Relation-like ) by FUNCT_1:def_2; ::_thesis: verum
end;
suppose x in dom C ; ::_thesis: ( C . x is segmental & C . x is Function-like & C . x is Relation-like )
hence  ( C . x is segmental & C . x is Function-like & C . x is Relation-like ) by Def14; ::_thesis: verum
end;
end;
end;
end;

registration
let O be non empty connected Poset;
let R be array of O;
let C be arr_computation of R;
let x be set ;
clusterC . x ->  the carrier of O -valued ;
coherence
 C . x is the carrier of O -valued
proof
percases ( x nin dom C or x in dom C ) ;
suppose x nin dom C ; ::_thesis: C . x is the carrier of O -valued
then  C . x = {} by FUNCT_1:def_2;
then  rng (C . x) = {} ;
hence  rng (C . x) c= the carrier of O by XBOOLE_1:2; :: according to RELAT_1:def_19 ::_thesis: verum
end;
suppose x in dom C ; ::_thesis: C . x is the carrier of O -valued
hence  C . x is the carrier of O -valued by Def14; ::_thesis: verum
end;
end;
end;
end;

registration
let O be non empty connected Poset;
let R be array of O;
let C be arr_computation of R;
cluster last C ->  Relation-like Function-like segmental ;
coherence
 ( last C is segmental & last C is Relation-like & last C is Function-like ) ;
end;

registration
let O be non empty connected Poset;
let R be array of O;
let C be arr_computation of R;
cluster last C ->  the carrier of O -valued ;
coherence
 last C is the carrier of O -valued ;
end;

definition
let O be non empty connected Poset;
let R be array of O;
let C be arr_computation of R;
attrC is complete  means :Def15: :: EXCHSORT:def 15
 last C is ascending ;
end;

:: deftheorem Def15 defines complete EXCHSORT:def_15_:_
 for O being non empty connected Poset
for R being array of O
for C being arr_computation of R holds
( C is complete iff last C is ascending );

theorem Th76: :: EXCHSORT:76
for O being non empty connected Poset
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
proof
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 H1( array of O) ->  set = card (inversions $1);
 base- C = 0 by Th24;
then A2: H1(C . 0) is finite by A1;
A3: for a being ordinal number st succ a in dom C & H1(C . a) is finite holds
H1(C . (succ a)) c< H1(C . a)
proof
let a be ordinal number ; ::_thesis: ( succ a in dom C & H1(C . a) is finite implies H1(C . (succ a)) c< H1(C . a) )
assume A4: ( succ a in dom C & H1(C . a) is finite ) ; ::_thesis: H1(C . (succ a)) c< H1(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  H1(C . (succ a)) in H1(C . a) by A5, Th73;
then  ( H1(C . (succ a)) c= H1(C . a) & H1(C . (succ a)) <> H1(C . a) ) by ORDINAL1:def_2;
hence  H1(C . (succ a)) c< H1(C . a) by XBOOLE_0:def_8; ::_thesis: verum
end;
thus  C is finite from EXCHSORT:sch_1(A2, A3); ::_thesis: verum
end;

theorem :: EXCHSORT:77
for O being non empty connected Poset
for R being array of O
for C being 0 -based arr_computation of R st R is finite array of O & ( for a being ordinal number st inversions (C . a) <> {} holds
succ a in dom C ) holds
C is complete
proof
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 & ( for a being ordinal number st inversions (C . a) <> {} holds
succ a in dom C ) holds
C is complete
let R be array of O; ::_thesis: for C being 0 -based arr_computation of R st R is finite array of O & ( for a being ordinal number st inversions (C . a) <> {} holds
succ a in dom C ) holds
C is complete
let C be 0 -based arr_computation of R; ::_thesis: ( R is finite array of O & ( for a being ordinal number st inversions (C . a) <> {} holds
succ a in dom C ) implies C is complete )
assume  R is finite array of O ; ::_thesis: ( ex a being ordinal number st
( inversions (C . a) <> {} & not succ a in dom C ) or C is complete )
then  C is finite by Th76;
then reconsider d = dom C as non empty finite Ordinal ;
assume A1: for a being ordinal number st inversions (C . a) <> {} holds
succ a in dom C ; ::_thesis: C is complete
set u = union d;
consider n being Nat such that
A2: d = n + 1 by NAT_1:6;
A3: d = succ n by A2, NAT_1:38;
then A4: union d = n by ORDINAL2:2;
 ( inversions (C . (union d)) <> 0 implies d in d ) by A1, A3, A4;
hence  last C is ascending by Th48; :: according to EXCHSORT:def_15 ::_thesis: verum
end;

theorem Th78: :: EXCHSORT:78
for O being non empty connected Poset
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 ) )
proof
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
A1: dom C = a \ b by Def1;
consider n being Nat such that
A2: a = b +^ n by A1, Th7;
defpred S9[ Nat] means ( b +^ $1 in dom C implies C . (b +^ $1) is permutation of R );
A3: b +^ 0 = b by ORDINAL2:27;
then  n <> 0 by A1, A2, XBOOLE_1:37;
then consider m being Nat such that
A4: n = m + 1 by NAT_1:6;
A5: a = b +^ (succ m) by A2, A4, NAT_1:38
.= succ (b +^ m) by ORDINAL2:28 ;
then A6: b +^ m = union a by ORDINAL2:2
.= union (a \ b) by A1, Th6 ;
 C . (base- C) = R by Def14;
then  C . b = R by A1, Th23;
then A7: S9[ 0 ] by A3, Th38;
A8: for k being Nat st S9[k] holds
S9[k + 1]
proof
let k be Nat; ::_thesis: ( S9[k] implies S9[k + 1] )
assume A9: ( S9[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 A10: b +^ (k + 1) = succ (b +^ k) by ORDINAL2:28;
then  ( b +^ k in b +^ (k + 1) & b +^ (k + 1) in a ) by A1, A9, ORDINAL1:6;
then A11: ( b c= b +^ k & b +^ k in a ) by ORDINAL1:10, ORDINAL3:24;
then  b +^ k in dom C by A1, ORDINAL6:5;
then consider Q being array of O, x, y being set  such that
A12: ( [x,y] in inversions Q & C . (b +^ k) = Q & C . (b +^ (k + 1)) = Swap (Q,x,y) ) by A9, A10, Def14;
 ( x in dom Q & y in dom Q ) by A12, Th46;
then  Swap (Q,x,y) is permutation of Q by Th43;
hence  C . (b +^ (k + 1)) is permutation of R by A9, A1, A11, A12, Th40, ORDINAL6:5; ::_thesis: verum
end;
A13: for k being Nat holds S9[k] from NAT_1:sch_2(A7, A8);
 ( b c= b +^ m & b +^ m in a ) by A5, ORDINAL1:6, ORDINAL3:24;
then  ( S9[m] & b +^ m in dom C ) by A1, A13, ORDINAL6:5;
hence  last C is permutation of R by A1, A6; ::_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 A14: c in dom C ; ::_thesis: C . c is permutation of R
then A15: ( b c= c & c in a ) by A1, ORDINAL6:5;
then  c = b +^ (c -^ b) by ORDINAL3:def_5;
then  c -^ b in n by A2, A14, A1, ORDINAL3:22;
then reconsider k = c -^ b as Nat ;
 S9[k] by A13;
hence  C . c is permutation of R by A14, A15, ORDINAL3:def_5; ::_thesis: verum
end;

begin

theorem Th79: :: EXCHSORT:79
for X being set
for A being finite 0 -based array of X st A <> {} holds
last A in X
proof
let X be set ; ::_thesis: for A being finite 0 -based array of X st A <> {} holds
last A in X
let A be finite 0 -based array of X; ::_thesis: ( A <> {} implies last A in X )
assume  A <> {} ; ::_thesis: last A in X
then consider n being Nat such that
A1: dom A = n + 1 by NAT_1:6;
 n + 1 = succ n by NAT_1:38;
then  ( n in dom A & union (dom A) = n ) by A1, ORDINAL1:6, ORDINAL2:2;
hence  last A in X by FUNCT_1:102; ::_thesis: verum
end;

theorem Th80: :: EXCHSORT:80
for x being set holds last <%x%> = x
proof
let x be set ; ::_thesis: last <%x%> = x
 dom <%x%> = succ 0 by AFINSQ_1:def_4;
then  union (dom <%x%>) = 0 by ORDINAL2:2;
hence  last <%x%> = x by AFINSQ_1:def_4; ::_thesis: verum
end;

theorem Th81: :: EXCHSORT:81
for x being set
for A being finite 0 -based array holds last (A ^ <%x%>) = x
proof
let x be set ; ::_thesis: for A being finite 0 -based array holds last (A ^ <%x%>) = x
let A be finite 0 -based array; ::_thesis: last (A ^ <%x%>) = x
 dom <%x%> = 1 by AFINSQ_1:def_4;
then  dom (A ^ <%x%>) = (dom A) +^ 1 by ORDINAL4:def_1
.= succ (dom A) by ORDINAL2:31 ;
then  union (dom (A ^ <%x%>)) = len A by ORDINAL2:2;
hence  last (A ^ <%x%>) = x by AFINSQ_1:36; ::_thesis: verum
end;

registration
let X be set ;
cluster  -> X -valued for Element of X ^omega ;
coherence
 for b1 being Element of X ^omega holds b1 is X -valued by AFINSQ_1:42;
end;

scheme :: EXCHSORT:sch 2
A{ F1( set ) ->  set , F2() ->  non empty set , P1[ set , set ], F3() ->  set } :
 ex f being non empty finite 0 -based array ex k being Element of F2() st
( k = last f & F1(k) = {} & f . 0 = F3() & ( for a being ordinal number st succ a in dom f holds
ex x, y being Element of F2() st
( x = f . a & y = f . (succ a) & P1[x,y] ) ) )
provided
A1: F3() in F2() and
A2: F1(F3()) is finite and
A3: for x being Element of F2() st F1(x) <> {} holds
ex y being Element of F2() st
( P1[x,y] & F1(y) c< F1(x) )
proof
set D = F2() ^omega ;
reconsider s0 = F3() as Element of F2() by A1;
reconsider f0 = <%s0%> as Element of F2() ^omega by AFINSQ_1:42;
defpred S9[ set , Element of F2() ^omega , Element of F2() ^omega ] means ( ( ( $2 = {} or F1((last $2)) = {} ) implies $2 = $3 ) & ( $2 <> {} & F1((last $2)) <> {} implies ex y being Element of F2() st
( P1[ last $2,y] & F1(y) c< F1((last $2)) & $2 ^ <%y%> = $3 ) ) );
A4: for a being Element of NAT
for x being Element of F2() ^omega ex y being Element of F2() ^omega st S9[a,x,y]
proof
let a be Element of NAT ; ::_thesis: for x being Element of F2() ^omega ex y being Element of F2() ^omega st S9[a,x,y]
let x be Element of F2() ^omega ; ::_thesis: ex y being Element of F2() ^omega st S9[a,x,y]
percases ( x = {} or F1((last x)) = {} or ( x <> {} & F1((last x)) <> {} ) ) ;
supposeA5: ( x = {} or F1((last x)) = {} ) ; ::_thesis: ex y being Element of F2() ^omega st S9[a,x,y]
take y = x; ::_thesis: S9[a,x,y]
thus  S9[a,x,y] by A5; ::_thesis: verum
end;
supposeA6: ( x <> {} & F1((last x)) <> {} ) ; ::_thesis: ex y being Element of F2() ^omega st S9[a,x,y]
then  last x in F2() by Th79;
then consider y being Element of F2() such that
A7: ( P1[ last x,y] & F1(y) c< F1((last x)) ) by A3, A6;
reconsider z = x ^ <%y%> as Element of F2() ^omega by AFINSQ_1:42;
take  z ; ::_thesis: S9[a,x,z]
thus  S9[a,x,z] by A6, A7; ::_thesis: verum
end;
end;
end;
consider F being Function of NAT,(F2() ^omega) such that
A8: ( F . 0 = f0 & ( for a being Element of NAT holds S9[a,F . a,F . (a + 1)] ) ) from RECDEF_1:sch_2(A4);
defpred S10[ Nat] means F . $1 <> {} ;
A9: S10[ 0 ] by A8;
A10: for m being Nat st S10[m] holds
S10[m + 1]
proof
let m be Nat; ::_thesis: ( S10[m] implies S10[m + 1] )
assume  S10[m] ; ::_thesis: S10[m + 1]
then reconsider f = F . m as non empty T-Sequence ;
 m in NAT by ORDINAL1:def_12;
then  S9[m,F . m,F . (m + 1)] by A8;
then  ( F . (m + 1) = f or ex x being set st F . (m + 1) = f ^ <%x%> ) ;
hence  S10[m + 1] ; ::_thesis: verum
end;
A11: for m being Nat holds S10[m] from NAT_1:sch_2(A9, A10);
defpred S11[ Function] means ( $1 . 0 = F3() & ( for a being ordinal number st succ a in dom $1 holds
ex x, y being Element of F2() st
( x = $1 . a & y = $1 . (succ a) & P1[x,y] ) ) );
defpred S12[ Nat] means S11[F . $1];
A12: S12[ 0 ]
proof
thus  (F . 0) . 0 = F3() by A8, AFINSQ_1:def_4; ::_thesis: for a being ordinal number st succ a in dom (F . 0) holds
ex x, y being Element of F2() st
( x = (F . 0) . a & y = (F . 0) . (succ a) & P1[x,y] )
let a be ordinal number ; ::_thesis: ( succ a in dom (F . 0) implies ex x, y being Element of F2() st
( x = (F . 0) . a & y = (F . 0) . (succ a) & P1[x,y] ) )
assume  succ a in dom (F . 0) ; ::_thesis: ex x, y being Element of F2() st
( x = (F . 0) . a & y = (F . 0) . (succ a) & P1[x,y] )
then  succ a in 1 by A8, AFINSQ_1:def_4;
hence  ex x, y being Element of F2() st
( x = (F . 0) . a & y = (F . 0) . (succ a) & P1[x,y] ) by CARD_1:49, TARSKI:def_1; ::_thesis: verum
end;
A13: for m being Nat st S12[m] holds
S12[m + 1]
proof
let m be Nat; ::_thesis: ( S12[m] implies S12[m + 1] )
assume A14: S12[m] ; ::_thesis: S12[m + 1]
A15: m in NAT by ORDINAL1:def_12;
then A16: S9[m,F . m,F . (m + 1)] by A8;
percases ( F . m = {} or F1((last (F . m))) = {} or ( F . m <> {} & F1((last (F . m))) <> {} ) ) ;
suppose ( F . m = {} or F1((last (F . m))) = {} ) ; ::_thesis: S12[m + 1]
hence  S12[m + 1] by A14, A16; ::_thesis: verum
end;
supposeA17: ( F . m <> {} & F1((last (F . m))) <> {} ) ; ::_thesis: S12[m + 1]
reconsider fm = F . m as non empty finite T-Sequence of by A17;
reconsider fm1 = F . (m + 1) as finite T-Sequence of ;
consider y being Element of F2() such that
A18: ( P1[ last fm,y] & F1(y) c< F1((last fm)) & fm ^ <%y%> = F . (m + 1) ) by A8, A15, A17;
 0 in dom fm by ORDINAL3:8;
hence  (F . (m + 1)) . 0 = F3() by A14, A18, ORDINAL4:def_1; ::_thesis: for a being ordinal number st succ a in dom (F . (m + 1)) holds
ex x, y being Element of F2() st
( x = (F . (m + 1)) . a & y = (F . (m + 1)) . (succ a) & P1[x,y] )
let a be ordinal number ; ::_thesis: ( succ a in dom (F . (m + 1)) implies ex x, y being Element of F2() st
( x = (F . (m + 1)) . a & y = (F . (m + 1)) . (succ a) & P1[x,y] ) )
assume A19: succ a in dom (F . (m + 1)) ; ::_thesis: ex x, y being Element of F2() st
( x = (F . (m + 1)) . a & y = (F . (m + 1)) . (succ a) & P1[x,y] )
A20: a in succ a by ORDINAL1:6;
then A21: a in dom fm1 by A19, ORDINAL1:10;
reconsider n = a as Nat by A19, A20;
reconsider x = fm1 . a, z = fm1 . (succ a) as Element of F2() by A19, A21, FUNCT_1:102;
A22: dom <%y%> = 1 by AFINSQ_1:def_4;
then  dom fm1 = (dom fm) +^ 1 by A18, ORDINAL4:def_1
.= succ (dom fm) by ORDINAL2:31 ;
then A23: a in dom fm by A19, ORDINAL3:3;
take  x ; ::_thesis: ex y being Element of F2() st
( x = (F . (m + 1)) . a & y = (F . (m + 1)) . (succ a) & P1[x,y] )
take  z ; ::_thesis: ( x = (F . (m + 1)) . a & z = (F . (m + 1)) . (succ a) & P1[x,z] )
thus  ( x = (F . (m + 1)) . a & z = (F . (m + 1)) . (succ a) ) ; ::_thesis: P1[x,z]
percases ( succ a in dom fm or dom fm c= succ a ) by ORDINAL6:4;
supposeA24: succ a in dom fm ; ::_thesis: P1[x,z]
then  a in dom fm by A20, ORDINAL1:10;
then A25: ( x = fm . a & z = fm . (succ a) ) by A18, A24, ORDINAL4:def_1;
 ex x, y being Element of F2() st
( x = fm . a & y = fm . (succ a) & P1[x,y] ) by A14, A24;
hence  P1[x,z] by A25; ::_thesis: verum
end;
supposeA26: dom fm c= succ a ; ::_thesis: P1[x,z]
 succ a c= dom fm by A23, ORDINAL1:21;
then A27: dom fm = succ a by A26, XBOOLE_0:def_10;
then  union (dom fm) = a by ORDINAL2:2;
then A28: last fm = fm1 . a by A18, A23, ORDINAL4:def_1;
 ( 0 in 1 & (succ a) +^ 0 = succ a ) by NAT_1:44, ORDINAL2:27;
then  z = <%y%> . 0 by A22, A18, A27, ORDINAL4:def_1;
hence  P1[x,z] by A18, A28, AFINSQ_1:def_4; ::_thesis: verum
end;
end;
end;
end;
end;
A29: for m being Nat holds S12[m] from NAT_1:sch_2(A12, A13);
defpred S13[ Nat] means  ex n being Nat st card F1((last (F . n))) = $1;
A30: ex n being Nat st S13[n]
proof
 last f0 = s0 by Th80;
then reconsider n = card F1((last (F . 0))) as Nat by A2, A8;
take  n ; ::_thesis: S13[n]
thus  S13[n] ; ::_thesis: verum
end;
A31: for n being Nat st n <> 0 & S13[n] holds
ex m being Nat st
( m < n & S13[m] )
proof
let n be Nat; ::_thesis: ( n <> 0 & S13[n] implies ex m being Nat st
( m < n & S13[m] ) )
assume A32: n <> 0 ; ::_thesis: ( not S13[n] or ex m being Nat st
( m < n & S13[m] ) )
given k being Nat such that A33: card F1((last (F . k))) = n ; ::_thesis: ex m being Nat st
( m < n & S13[m] )
reconsider fk = F . k, fk1 = F . (k + 1) as Element of F2() ^omega ;
 k in NAT by ORDINAL1:def_12;
then  ( S9[k,fk,fk1] & fk <> {} ) by A11, A8;
then consider y being Element of F2() such that
A34: ( P1[ last fk,y] & F1(y) c< F1((last fk)) & fk ^ <%y%> = fk1 ) by A32, A33;
A35: ( F1((last fk)) is finite & F1(y) c= F1((last fk)) ) by A33, A34, XBOOLE_0:def_8;
A36: last fk1 = y by A34, Th81;
then reconsider m = card F1((last fk1)) as Nat by A35;
take  m ; ::_thesis: ( m < n & S13[m] )
thus  m < n by A33, A34, A35, A36, TREES_1:6; ::_thesis: S13[m]
thus  S13[m] ; ::_thesis: verum
end;
 S13[ 0 ] from NAT_1:sch_7(A30, A31);
then consider n being Nat such that
A37: card F1((last (F . n))) = 0 ;
reconsider f = F . n as non empty XFinSequence of by A11;
take  f ; ::_thesis: ex k being Element of F2() st
( k = last f & F1(k) = {} & f . 0 = F3() & ( for a being ordinal number st succ a in dom f holds
ex x, y being Element of F2() st
( x = f . a & y = f . (succ a) & P1[x,y] ) ) )
reconsider k = last f as Element of F2() by Th79;
take  k ; ::_thesis: ( k = last f & F1(k) = {} & f . 0 = F3() & ( for a being ordinal number st succ a in dom f holds
ex x, y being Element of F2() st
( x = f . a & y = f . (succ a) & P1[x,y] ) ) )
thus  ( k = last f & F1(k) = {} ) by A37; ::_thesis: ( f . 0 = F3() & ( for a being ordinal number st succ a in dom f holds
ex x, y being Element of F2() st
( x = f . a & y = f . (succ a) & P1[x,y] ) ) )
thus  S11[f] by A29; ::_thesis: verum
end;


theorem Th82: :: EXCHSORT:82
for A being array
for B being permutation of A holds B in Funcs ((dom A),(rng A))
proof
let A be array; ::_thesis: for B being permutation of A holds B in Funcs ((dom A),(rng A))
let B be permutation of A; ::_thesis: B in Funcs ((dom A),(rng A))
 ( dom B = dom A & rng B = rng A ) by Th37;
hence  B in Funcs ((dom A),(rng A)) by FUNCT_2:def_2; ::_thesis: verum
end;

registration
let A be real-valued array;
cluster  ->  real-valued for permutation of A;
coherence
 for b1 being permutation of A holds b1 is real-valued
proof
let B be permutation of A; ::_thesis: B is real-valued
 ex f being Permutation of (dom A) st B = A * f by Def9;
hence  B is real-valued ; ::_thesis: verum
end;
end;

registration
let a be ordinal number ;
let X be non empty set ;
cluster  ->  T-Sequence-like for Element of Funcs (a,X);
coherence
 for b1 being Element of Funcs (a,X) holds b1 is T-Sequence-like
proof
let x be Element of Funcs (a,X); ::_thesis: x is T-Sequence-like
 dom x = a by FUNCT_2:92;
hence  x is T-Sequence-like by ORDINAL1:def_7; ::_thesis: verum
end;
end;

registration
let X be set ;
let Y be real-membered non empty set ;
cluster  ->  real-valued for Element of Funcs (X,Y);
coherence
 for b1 being Element of Funcs (X,Y) holds b1 is real-valued ;
end;

registration
let X be set ;
let A be array of X;
cluster  -> X -valued for permutation of A;
coherence
 for b1 being permutation of A holds b1 is X -valued
proof
let B be permutation of A; ::_thesis: B is X -valued
 ex f being Permutation of (dom A) st B = A * f by Def9;
hence  B is X -valued ; ::_thesis: verum
end;
end;

registration
let X, Z be set ;
let Y be Subset of Z;
cluster  -> Z -valued for Element of Funcs (X,Y);
coherence
 for b1 being Element of Funcs (X,Y) holds b1 is Z -valued
proof
let f be Element of Funcs (X,Y); ::_thesis: f is Z -valued
percases ( f = {} or Funcs (X,Y) <> {} ) by SUBSET_1:def_1;
suppose f = {} ; ::_thesis: f is Z -valued
then  rng f = {} ;
hence  rng f c= Z by XBOOLE_1:2; :: according to RELAT_1:def_19 ::_thesis: verum
end;
suppose Funcs (X,Y) <> {} ; ::_thesis: f is Z -valued
then  rng f c= Y by FUNCT_2:92;
hence  rng f c= Z by XBOOLE_1:1; :: according to RELAT_1:def_19 ::_thesis: verum
end;
end;
end;
end;

theorem :: EXCHSORT:83
for X, Y being set
for r being b1 -defined b2 -valued Relation holds r is Relation of X,Y
proof
let X, Y be set ; ::_thesis: for r being X -defined Y -valued Relation holds r is Relation of X,Y
let r be X -defined Y -valued Relation; ::_thesis: r is Relation of X,Y
 ( [:(dom r),(rng r):] c= [:X,Y:] & r c= [:(dom r),(rng r):] ) by RELAT_1:7, ZFMISC_1:96;
hence  r is Relation of X,Y by XBOOLE_1:1; ::_thesis: verum
end;

theorem Th84: :: EXCHSORT:84
for a being finite Ordinal
for x being set holds
( not x in a or x = 0 or ex b being ordinal number st x = succ b )
proof
let a be finite Ordinal; ::_thesis: for x being set holds
( not x in a or x = 0 or ex b being ordinal number st x = succ b )
let x be set ; ::_thesis: ( not x in a or x = 0 or ex b being ordinal number st x = succ b )
assume A1: ( x in a & x <> 0 ) ; ::_thesis: ex b being ordinal number st x = succ b
then A2: {} in x by ORDINAL3:8;
now__::_thesis:_not_x_is_limit_ordinal
assume  x is limit_ordinal ; ::_thesis: contradiction
then  ( omega c= x & x c= a ) by A1, A2, ORDINAL1:def_2, ORDINAL1:def_11;
hence  contradiction ; ::_thesis: verum
end;
hence  ex b being ordinal number st x = succ b by A1, ORDINAL1:29; ::_thesis: verum
end;

theorem Th85: :: EXCHSORT:85
for O being non empty connected Poset
for A being non empty finite 0 -based array of O ex C being 0 -based arr_computation of A st C is complete
proof
let O be non empty connected Poset; ::_thesis: for A being non empty finite 0 -based array of O ex C being 0 -based arr_computation of A st C is complete
let A be non empty finite 0 -based array of O; ::_thesis: ex C being 0 -based arr_computation of A st C is complete
reconsider rA = rng A as non empty Subset of O by RELAT_1:def_19;
reconsider a = dom A as Ordinal ;
set X = Funcs (a,rA);
deffunc H1( array of O) ->  set = card (inversions $1);
defpred S9[ Element of Funcs (a,rA), Element of Funcs (a,rA)] means  ex p, q being Element of dom A st
( [p,q] in inversions $1 & $2 = Swap ($1,p,q) );
 A is permutation of A by Th38;
then A1: A in Funcs (a,rA) by Th82;
A2: H1(A) is finite ;
A3: for x being Element of Funcs (a,rA) st H1(x) <> {} holds
ex y being Element of Funcs (a,rA) st
( S9[x,y] & H1(y) c< H1(x) )
proof
let x be Element of Funcs (a,rA); ::_thesis: ( H1(x) <> {} implies ex y being Element of Funcs (a,rA) st
( S9[x,y] & H1(y) c< H1(x) ) )
reconsider c = x as array of O ;
set z = the Element of inversions c;
set Fx = H1(x);
assume  H1(x) <> {} ; ::_thesis: ex y being Element of Funcs (a,rA) st
( S9[x,y] & H1(y) c< H1(x) )
then A4: inversions c <> {} ;
then  ( the Element of inversions c in inversions c & inversions c is Relation of (dom x),(dom x) ) by Th47;
then consider p, q being set  such that
A5: ( the Element of inversions c = [p,q] & p in dom x & q in dom x ) by RELSET_1:2;
set y = Swap (x,p,q);
A6: ( dom (Swap (x,p,q)) = dom x & rng (Swap (x,p,q)) = rng x ) by FUNCT_7:99, FUNCT_7:103;
 ( dom x = dom A & rng x c= rng A ) by FUNCT_2:92;
then reconsider y = Swap (x,p,q) as Element of Funcs (a,rA) by A6, FUNCT_2:def_2;
reconsider b = y as array of O ;
set Fy = H1(y);
take  y ; ::_thesis: ( S9[x,y] & H1(y) c< H1(x) )
thus  S9[x,y] by A4, A5; ::_thesis: H1(y) c< H1(x)
 H1(b) in H1(c) by A4, A5, Th73;
hence  ( H1(y) c= H1(x) & H1(y) <> H1(x) ) by ORDINAL1:def_2; :: according to XBOOLE_0:def_8 ::_thesis: verum
end;
consider f being non empty finite 0 -based array, k being Element of Funcs (a,rA) such that
A7: ( k = last f & H1(k) = {} & f . 0 = A ) and
A8: for a being ordinal number st succ a in dom f holds
ex x, y being Element of Funcs (a,rA) st
( x = f . a & y = f . (succ a) & S9[x,y] ) from EXCHSORT:sch_2(A1, A2, A3);
 f is arr_computation of A
proof
thus  f . (base- f) = A by A7, Th24; :: according to EXCHSORT:def_14 ::_thesis: ( ( for a being ordinal number st a in dom f holds
f . a is array of O ) & ( for a being ordinal number st a in dom f & succ a in dom f holds
ex R being array of O ex x, y being set st
( [x,y] in inversions R & f . a = R & f . (succ a) = Swap (R,x,y) ) ) )
thus  for a being ordinal number st a in dom f holds
f . a is array of O ::_thesis: for a being ordinal number st a in dom f & succ a in dom f holds
ex R being array of O ex x, y being set st
( [x,y] in inversions R & f . a = R & f . (succ a) = Swap (R,x,y) )
proof
let a be ordinal number ; ::_thesis: ( a in dom f implies f . a is array of O )
assume A9: a in dom f ; ::_thesis: f . a is array of O
percases ( a = 0 or ex b being ordinal number st a = succ b ) by A9, Th84;
suppose a = 0 ; ::_thesis: f . a is array of O
hence  f . a is array of O by A7; ::_thesis: verum
end;
suppose ex b being ordinal number st a = succ b ; ::_thesis: f . a is array of O
then consider b being ordinal number  such that
A10: a = succ b ;
 ex x, y being Element of Funcs (a,rA) st
( x = f . b & y = f . a & S9[x,y] ) by A8, A9, A10;
hence  f . a is array of O ; ::_thesis: verum
end;
end;
end;
let a be ordinal number ; ::_thesis: ( a in dom f & succ a in dom f implies ex R being array of O ex x, y being set st
( [x,y] in inversions R & f . a = R & f . (succ a) = Swap (R,x,y) ) )
assume  ( a in dom f & succ a in dom f ) ; ::_thesis: ex R being array of O ex x, y being set st
( [x,y] in inversions R & f . a = R & f . (succ a) = Swap (R,x,y) )
then  ex x, y being Element of Funcs (a,rA) st
( x = f . a & y = f . (succ a) & S9[x,y] ) by A8;
hence  ex R being array of O ex x, y being set st
( [x,y] in inversions R & f . a = R & f . (succ a) = Swap (R,x,y) ) ; ::_thesis: verum
end;
then reconsider f = f as 0 -based arr_computation of A ;
take  f ; ::_thesis: f is complete
 inversions (last f) = {} by A7;
hence  last f is ascending by Th48; :: according to EXCHSORT:def_15 ::_thesis: verum
end;

theorem Th86: :: EXCHSORT:86
for O being non empty connected Poset
for A being non empty finite 0 -based array of O ex B being permutation of A st B is ascending
proof
let O be non empty connected Poset; ::_thesis: for A being non empty finite 0 -based array of O ex B being permutation of A st B is ascending
let A be non empty finite 0 -based array of O; ::_thesis: ex B being permutation of A st B is ascending
consider C being 0 -based arr_computation of A such that
A1: C is complete by Th85;
 C is finite by Th76;
then reconsider B = last C as permutation of A by Th78;
take  B ; ::_thesis: B is ascending
thus  B is ascending by A1, Def15; ::_thesis: verum
end;

registration
let O be non empty connected Poset;
let A be finite 0 -based array of O;
cluster Relation-like the carrier of O -valued Function-like segmental ascending for permutation of A;
existence
 ex b1 being permutation of A st b1 is ascending
proof
A1: A is permutation of A by Th38;
 ( A is empty implies A is ascending ) ;
hence  ex b1 being permutation of A st b1 is ascending by A1, Th86; ::_thesis: verum
end;
end;