let p9, q9 be FinSequence of X; :: thesis:
assume that
A42: rng p9 = A and
A43: for n, m being Nat st n in dom p9 & m in dom p9 & n < m holds
( p9 /. n <> p9 /. m & [(p9 /. n),(p9 /. m)] in R ) and
A44: rng q9 = A and
A45: for n, m being Nat st n in dom q9 & m in dom q9 & n < m holds
( q9 /. n <> q9 /. m & [(q9 /. n),(q9 /. m)] in R ) ; :: thesis:

then p9 is empty by A42;
hence p9 = q9 by A44, A46; :: thesis:

end;

suppose A47: not A is empty ; :: thesis:

then reconsider X9 = X as non empty set ;
reconsider A9 = A as non empty finite Subset of X9 by A47;
reconsider R9 = R as Order of X9 ;
set E = <*> A9;
defpred S₁[ FinSequence of A9] means ( $1 is FinSequence of A9 & ( for n, m being Nat st n in dom $1 & m in dom $1 & n < m holds
( $1 /. n <> $1 /. m & [($1 /. n),($1 /. m)] in R ) ) implies for q being FinSequence of A9 st rng q = rng $1 & ( for n, m being Nat st n in dom q & m in dom q & n < m holds
( q /. n <> q /. m & [(q /. n),(q /. m)] in R ) ) holds
q = $1 );
reconsider p = p9, q = q9 as FinSequence of A9 by A42, A44, FINSEQ_1:def 4;
A48: for p being FinSequence of A9
for x being Element of A9 st S₁[p] holds
S₁[p ^ <*x*>]

proof

let p be FinSequence of A9; :: thesis:
let x be Element of A9; :: thesis:
assume A49: S₁[p] ; :: thesis:
assume p ^ <*x*> is FinSequence of A9 ; :: thesis:
assume A50: for n, m being Nat st n in dom (p ^ <*x*>) & m in dom (p ^ <*x*>) & n < m holds
( (p ^ <*x*>) /. n <> (p ^ <*x*>) /. m & [((p ^ <*x*>) /. n),((p ^ <*x*>) /. m)] in R ) ; :: thesis:
let q be FinSequence of A9; :: thesis:
assume that
A51: rng q = rng (p ^ <*x*>) and
A52: for n, m being Nat st n in dom q & m in dom q & n < m holds
( q /. n <> q /. m & [(q /. n),(q /. m)] in R ) ; :: thesis:
deffunc H₁( Nat) -> set = q . $1;
A53: q <> 0 by A51;
then consider n being Nat such that
A54: len q = n + 1 by NAT_1:6;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
ex q9 being FinSequence st
( len q9 = n & ( for m being Nat st m in dom q9 holds
q9 . m = H₁(m) ) ) from FINSEQ_1:sch 2();
then consider q9 being FinSequence such that
A55: len q9 = n and
A56: for m being Nat st m in dom q9 holds
q9 . m = q . m ;
1 in Seg 1 by FINSEQ_1:4, TARSKI:def 1;
then A57: 1 in dom <*x*> by FINSEQ_1:def 8;
A58: ex m being Element of A9 st
( m = x & ( for l being Element of A9 st l in rng (p ^ <*x*>) & l <> x holds
[l,m] in R ) )

proof

reconsider m = x as Element of A9 ;
take m ; :: thesis:
thus m = x ; :: thesis:
thus for l being Element of A9 st l in rng (p ^ <*x*>) & l <> x holds
[l,m] in R :: thesis:

proof

let l be Element of A9; :: thesis:
assume that
A59: l in rng (p ^ <*x*>) and
A60: l <> x ; :: thesis:
consider y being set such that
A61: y in dom (p ^ <*x*>) and
A62: l = (p ^ <*x*>) . y by A59, FUNCT_1:def 5;
A63: l = (p ^ <*x*>) /. y by A61, A62, PARTFUN1:def 8;
reconsider k = y as Element of NAT by A61;
A64: k <> (len p) + 1

proof

assume k = (len p) + 1 ; :: thesis:
then (p ^ <*x*>) . k = <*x*> . 1 by A57, FINSEQ_1:def 7
.= x by FINSEQ_1:def 8 ;
hence contradiction by A60, A62; :: thesis:

end;

A65: y in Seg (len (p ^ <*x*>)) by A61, FINSEQ_1:def 3;
then k <= len (p ^ <*x*>) by FINSEQ_1:3;
then k <= (len p) + (len <*x*>) by FINSEQ_1:35;
then k <= (len p) + 1 by FINSEQ_1:56;
then k < (len p) + 1 by A64, XXREAL_0:1;
then k < (len p) + (len <*x*>) by FINSEQ_1:56;
then A66: k < len (p ^ <*x*>) by FINSEQ_1:35;
1 <= k by A65, FINSEQ_1:3;
then 1 - (len (p ^ <*x*>)) < k - k by A66, XREAL_1:17;
then 1 < len (p ^ <*x*>) by XREAL_1:50;
then len (p ^ <*x*>) in Seg (len (p ^ <*x*>)) by FINSEQ_1:3;
then A67: len (p ^ <*x*>) in dom (p ^ <*x*>) by FINSEQ_1:def 3;
m = (p ^ <*x*>) . ((len p) + 1) by FINSEQ_1:59
.= (p ^ <*x*>) . ((len p) + (len <*x*>)) by FINSEQ_1:56
.= (p ^ <*x*>) . (len (p ^ <*x*>)) by FINSEQ_1:35 ;
then m = (p ^ <*x*>) /. (len (p ^ <*x*>)) by A67, PARTFUN1:def 8;
hence [l,m] in R by A50, A61, A63, A66, A67; :: thesis:

end;

A68: for m being Nat st m in dom <*x*> holds
q . ((len q9) + m) = <*x*> . m

proof

let m be Nat; :: thesis:
assume m in dom <*x*> ; :: thesis:
then A69: m in {1} by FINSEQ_1:4, FINSEQ_1:def 8;
A70: q . ((len q9) + m) = x

proof

consider d1 being Element of A9 such that
A71: d1 = x and
A72: for l being Element of A9 st l in rng (p ^ <*x*>) & l <> x holds
[l,d1] in R by A58;
reconsider d = d1 as Element of A9 ;
len q in Seg (len q) by A53, FINSEQ_1:5;
then A74: len q in dom q by FINSEQ_1:def 3;
then q . (len q) in rng q by FUNCT_1:def 5;
then reconsider k = q . (len q) as Element of A9 ;
A75: k = q /. (len q) by A74, PARTFUN1:def 8;
field R = X by ORDERS_1:97;
then A76: R is_antisymmetric_in X by RELAT_2:def 12;
assume q . ((len q9) + m) <> x ; :: thesis:
then A78: q . (len q) <> x by A54, A55, A69, TARSKI:def 1;
x in {x} by TARSKI:def 1;
then x in rng <*x*> by FINSEQ_1:55;
then x in (rng p) \/ (rng <*x*>) by XBOOLE_0:def 3;
then x in rng q by A51, FINSEQ_1:44;
then consider y being set such that
A79: y in dom q and
A80: x = q . y by FUNCT_1:def 5;
A81: y in Seg (len q) by A79, FINSEQ_1:def 3;
reconsider y = y as Element of NAT by A79;
y <= len q by A81, FINSEQ_1:3;
then A82: y < len q by A78, A80, XXREAL_0:1;
q . (len q) in rng (p ^ <*x*>) by A51, A74, FUNCT_1:def 5;
then A83: [k,d] in R by A78, A72;
A85: d = q /. y by A71, A79, A80, PARTFUN1:def 8;
then A86: [d,k] in R by A52, A79, A74, A82, A75;
k <> d by A52, A79, A74, A82, A75, A85;
hence contradiction by A83, A86, A76, RELAT_2:def 4; :: thesis:

end;

m = 1 by A69, TARSKI:def 1;
hence q . ((len q9) + m) = <*x*> . m by A70, FINSEQ_1:57; :: thesis:

end;

now

let x be set ; :: thesis:
A87: n <= n + 1 by NAT_1:11;
assume x in rng q9 ; :: thesis:
then consider y being set such that
A88: y in dom q9 and
A89: x = q9 . y by FUNCT_1:def 5;
A90: y in Seg (len q9) by A88, FINSEQ_1:def 3;
reconsider y = y as Element of NAT by A88;
y <= n by A55, A90, FINSEQ_1:3;
then A91: y <= n + 1 by A87, XXREAL_0:2;
1 <= y by A90, FINSEQ_1:3;
then y in dom q by A54, A91, FINSEQ_3:27;
then q . y in rng q by FUNCT_1:def 5;
then q . y in A9 ;
hence x in A9 by A56, A88, A89; :: thesis:

end;

then rng q9 c= A9 by TARSKI:def 3;
then reconsider f = q9 as FinSequence of A9 by FINSEQ_1:def 4;
dom q = Seg (n + 1) by A54, FINSEQ_1:def 3
.= Seg ((len q9) + (len <*x*>)) by A55, FINSEQ_1:56 ;
then A93: q9 ^ <*x*> = q by A56, A68, FINSEQ_1:def 7;
A94: not x in rng p

proof

(len p) + 1 = (len p) + (len <*x*>) by FINSEQ_1:56
.= len (p ^ <*x*>) by FINSEQ_1:35 ;
then (len p) + 1 in Seg (len (p ^ <*x*>)) by FINSEQ_1:6;
then A95: (len p) + 1 in dom (p ^ <*x*>) by FINSEQ_1:def 3;
assume x in rng p ; :: thesis:
then consider y being set such that
A96: y in dom p and
A97: x = p . y by FUNCT_1:def 5;
A98: y in Seg (len p) by A96, FINSEQ_1:def 3;
A99: dom p c= dom (p ^ <*x*>) by FINSEQ_1:39;
reconsider y = y as Element of NAT by A96;
x = (p ^ <*x*>) . y by A96, A97, FINSEQ_1:def 7;
then A100: x = (p ^ <*x*>) /. y by A96, A99, PARTFUN1:def 8;
y <= len p by A98, FINSEQ_1:3;
then A101: y < (len p) + 1 by NAT_1:13;
x = (p ^ <*x*>) . ((len p) + 1) by FINSEQ_1:59;
then (p ^ <*x*>) /. y = (p ^ <*x*>) /. ((len p) + 1) by A95, A100, PARTFUN1:def 8;
hence contradiction by A50, A96, A95, A99, A101; :: thesis:

end;

A102: for z being set holds
( z in ((rng p) \/ {x}) \ {x} iff z in rng p )

proof

let z be set ; :: thesis:
thus ( z in ((rng p) \/ {x}) \ {x} implies z in rng p ) :: thesis:

proof

assume A103: z in ((rng p) \/ {x}) \ {x} ; :: thesis:
then X: not z in {x} by XBOOLE_0:def 5;
z in (rng p) \/ {x} by A103, XBOOLE_0:def 5;
hence z in rng p by XBOOLE_0:def 3, X; :: thesis:

end;

assume A104: z in rng p ; :: thesis:
then A105: z in (rng p) \/ {x} by XBOOLE_0:def 3;
not z in {x} by A94, A104, TARSKI:def 1;
hence z in ((rng p) \/ {x}) \ {x} by A105, XBOOLE_0:def 5; :: thesis:

end;

rng (p ^ <*x*>) = (rng p) \/ (rng <*x*>) by FINSEQ_1:44
.= (rng p) \/ {x} by FINSEQ_1:56 ;
then A106: rng p = (rng (p ^ <*x*>)) \ {x} by A102, TARSKI:2;
A107: ( rng f = rng p & ( for l, m being Nat st l in dom f & m in dom f & l < m holds
( f /. l <> f /. m & [(f /. l),(f /. m)] in R ) ) )

proof

A108: not x in rng f

proof

(len f) + 1 = (len f) + (len <*x*>) by FINSEQ_1:56
.= len (f ^ <*x*>) by FINSEQ_1:35 ;
then (len f) + 1 in Seg (len (f ^ <*x*>)) by FINSEQ_1:6;
then A109: (len f) + 1 in dom (f ^ <*x*>) by FINSEQ_1:def 3;
assume x in rng f ; :: thesis:
then consider y being set such that
A110: y in dom f and
A111: x = f . y by FUNCT_1:def 5;
A112: y in Seg (len f) by A110, FINSEQ_1:def 3;
A113: dom f c= dom (f ^ <*x*>) by FINSEQ_1:39;
reconsider y = y as Element of NAT by A110;
x = q . y by A56, A110, A111;
then A114: x = q /. y by A93, A110, A113, PARTFUN1:def 8;
y <= len f by A112, FINSEQ_1:3;
then A115: y < (len f) + 1 by NAT_1:13;
x = q . ((len f) + 1) by A93, FINSEQ_1:59;
then q /. y = q /. ((len f) + 1) by A93, A109, A114, PARTFUN1:def 8;
hence contradiction by A52, A93, A110, A109, A113, A115; :: thesis:

end;

A116: for z being set holds
( z in ((rng f) \/ {x}) \ {x} iff z in rng f )

proof

let z be set ; :: thesis:

hereby :: thesis:

assume A117: z in ((rng f) \/ {x}) \ {x} ; :: thesis:
then X: not z in {x} by XBOOLE_0:def 5;
z in (rng f) \/ {x} by A117, XBOOLE_0:def 5;
hence z in rng f by XBOOLE_0:def 3, X; :: thesis:

end;

assume A118: z in rng f ; :: thesis:
then A119: z in (rng f) \/ {x} by XBOOLE_0:def 3;
not z in {x} by A108, A118, TARSKI:def 1;
hence z in ((rng f) \/ {x}) \ {x} by A119, XBOOLE_0:def 5; :: thesis:

end;

rng (f ^ <*x*>) = (rng f) \/ (rng <*x*>) by FINSEQ_1:44
.= (rng f) \/ {x} by FINSEQ_1:56 ;
hence rng f = rng p by A51, A93, A106, A116, TARSKI:2; :: thesis:
let l, m be Nat; :: thesis:
assume that
A120: l in dom f and
A121: m in dom f and
A122: l < m ; :: thesis:
A123: f . m = f /. m by A121, PARTFUN1:def 8;
A124: dom f c= dom q by A93, FINSEQ_1:39;
then q . m = q /. m by A121, PARTFUN1:def 8;
then A125: f /. m = q /. m by A56, A121, A123;
A126: f . l = f /. l by A120, PARTFUN1:def 8;
q . l = q /. l by A124, A120, PARTFUN1:def 8;
then f /. l = q /. l by A56, A120, A126;
hence ( f /. l <> f /. m & [(f /. l),(f /. m)] in R ) by A52, A124, A120, A121, A122, A125; :: thesis:

end;

( p is FinSequence of A9 & ( for l, m being Nat st l in dom p & m in dom p & l < m holds
( p /. l <> p /. m & [(p /. l),(p /. m)] in R ) ) )

proof

thus p is FinSequence of A9 ; :: thesis:
let l, m be Nat; :: thesis:
assume that
A127: l in dom p and
A128: m in dom p and
A129: l < m ; :: thesis:
A130: dom p c= dom (p ^ <*x*>) by FINSEQ_1:39;
p . m = (p ^ <*x*>) . m by A128, FINSEQ_1:def 7;
then p . m = (p ^ <*x*>) /. m by A128, A130, PARTFUN1:def 8;
then A131: p /. m = (p ^ <*x*>) /. m by A128, PARTFUN1:def 8;
p . l = (p ^ <*x*>) . l by A127, FINSEQ_1:def 7;
then p . l = (p ^ <*x*>) /. l by A127, A130, PARTFUN1:def 8;
then p /. l = (p ^ <*x*>) /. l by A127, PARTFUN1:def 8;
hence ( p /. l <> p /. m & [(p /. l),(p /. m)] in R ) by A50, A127, A128, A129, A130, A131; :: thesis:

end;

hence q = p ^ <*x*> by A49, A93, A107; :: thesis:

end;

A132: now

let n, m be Nat; :: thesis:
assume that
A133: n in dom p and
A134: m in dom p and
A135: n < m ; :: thesis:
A136: p /. m = p . m by A134, PARTFUN1:def 8
.= p9 /. m by A134, PARTFUN1:def 8 ;
p /. n = p . n by A133, PARTFUN1:def 8
.= p9 /. n by A133, PARTFUN1:def 8 ;
hence ( p /. n <> p /. m & [(p /. n),(p /. m)] in R ) by A43, A133, A134, A135, A136; :: thesis:

end;

A137: now

let n, m be Nat; :: thesis:
assume that
A138: n in dom q and
A139: m in dom q and
A140: n < m ; :: thesis:
A141: q /. m = q . m by A139, PARTFUN1:def 8
.= q9 /. m by A139, PARTFUN1:def 8 ;
q /. n = q . n by A138, PARTFUN1:def 8
.= q9 /. n by A138, PARTFUN1:def 8 ;
hence ( q /. n <> q /. m & [(q /. n),(q /. m)] in R ) by A45, A138, A139, A140, A141; :: thesis:

end;

A142: S₁[ <*> A9] ;
for p being FinSequence of A9 holds S₁[p] from FINSEQ_2:sch 2(A142, A48);
hence p9 = q9 by A42, A44, A132, A137; :: thesis:

end;