let p9, q9 be FinSequence of X; :: thesis:
assume that
A59: rng p9 = A and
A60: 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
A61: rng q9 = A and
A62: 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 A59;
hence p9 = q9 by A61, A63; :: thesis:

end;

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

then reconsider X9 = X as non empty set ;
reconsider A9 = A as non empty finite Subset of X9 by A64;
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 A59, A61, FINSEQ_1:def 4;
A65: 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 A66: S₁[p] ; :: thesis:
assume p ^ <*x*> is FinSequence of A9 ; :: thesis:
assume A67: 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
A68: rng q = rng (p ^ <*x*>) and
A69: 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;
A70: q <> 0 by A68;
then consider n being Nat such that
A71: len q = n + 1 by NAT_1:6;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
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
A72: len q9 = n and
A73: for m being Nat st m in dom q9 holds
q9 . m = q . m ;
1 in Seg 1 by FINSEQ_1:2, TARSKI:def 1;
then A74: 1 in dom <*x*> by FINSEQ_1:def 8;
A75: 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
A76: l in rng (p ^ <*x*>) and
A77: l <> x ; :: thesis:
consider y being object such that
A78: y in dom (p ^ <*x*>) and
A79: l = (p ^ <*x*>) . y by A76, FUNCT_1:def 3;
A80: l = (p ^ <*x*>) /. y by A78, A79, PARTFUN1:def 6;
reconsider k = y as Element of NAT by A78;
A81: k <> (len p) + 1

proof

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

end;

A82: y in Seg (len (p ^ <*x*>)) by A78, FINSEQ_1:def 3;
then k <= len (p ^ <*x*>) by FINSEQ_1:1;
then k <= (len p) + (len <*x*>) by FINSEQ_1:22;
then k <= (len p) + 1 by FINSEQ_1:39;
then k < (len p) + 1 by A81, XXREAL_0:1;
then k < (len p) + (len <*x*>) by FINSEQ_1:39;
then A83: k < len (p ^ <*x*>) by FINSEQ_1:22;
1 <= k by A82, FINSEQ_1:1;
then 1 - (len (p ^ <*x*>)) < k - k by A83, XREAL_1:15;
then 1 < len (p ^ <*x*>) by XREAL_1:48;
then len (p ^ <*x*>) in Seg (len (p ^ <*x*>)) by FINSEQ_1:1;
then A84: len (p ^ <*x*>) in dom (p ^ <*x*>) by FINSEQ_1:def 3;
m = (p ^ <*x*>) . ((len p) + 1) by FINSEQ_1:42
.= (p ^ <*x*>) . ((len p) + (len <*x*>)) by FINSEQ_1:39
.= (p ^ <*x*>) . (len (p ^ <*x*>)) by FINSEQ_1:22 ;
then m = (p ^ <*x*>) /. (len (p ^ <*x*>)) by A84, PARTFUN1:def 6;
hence [l,m] in R by A67, A78, A80, A83, A84; :: thesis:

end;

A85: 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 A86: m in {1} by FINSEQ_1:2, FINSEQ_1:def 8;
A87: q . ((len q9) + m) = x

proof

consider d1 being Element of A9 such that
A88: d1 = x and
A89: for l being Element of A9 st l in rng (p ^ <*x*>) & l <> x holds
[l,d1] in R by A75;
reconsider d = d1 as Element of A9 ;
len q in Seg (len q) by A70, FINSEQ_1:3;
then A90: len q in dom q by FINSEQ_1:def 3;
then q . (len q) in rng q by FUNCT_1:def 3;
then reconsider k = q . (len q) as Element of A9 ;
A91: k = q /. (len q) by A90, PARTFUN1:def 6;
A92: field R = X by ORDERS_1:12;
assume q . ((len q9) + m) <> x ; :: thesis:
then A93: q . (len q) <> x by A71, A72, A86, TARSKI:def 1;
x in {x} by TARSKI:def 1;
then x in rng <*x*> by FINSEQ_1:38;
then x in (rng p) \/ (rng <*x*>) by XBOOLE_0:def 3;
then x in rng q by A68, FINSEQ_1:31;
then consider y being object such that
A94: y in dom q and
A95: x = q . y by FUNCT_1:def 3;
A96: y in Seg (len q) by A94, FINSEQ_1:def 3;
reconsider y = y as Element of NAT by A94;
y <= len q by A96, FINSEQ_1:1;
then A97: y < len q by A93, A95, XXREAL_0:1;
q . (len q) in rng (p ^ <*x*>) by A68, A90, FUNCT_1:def 3;
then A98: [k,d] in R by A93, A89;
A99: d = q /. y by A88, A94, A95, PARTFUN1:def 6;
then A100: [d,k] in R by A69, A94, A90, A97, A91;
k <> d by A69, A94, A90, A97, A91, A99;
hence contradiction by A98, A100, A92, RELAT_2:def 4, RELAT_2:def 12; :: thesis:

end;

m = 1 by A86, TARSKI:def 1;
hence q . ((len q9) + m) = <*x*> . m by A87, FINSEQ_1:40; :: thesis:

end;

now :: thesis:

let x be object ; :: thesis:
A101: n <= n + 1 by NAT_1:11;
assume x in rng q9 ; :: thesis:
then consider y being object such that
A102: y in dom q9 and
A103: x = q9 . y by FUNCT_1:def 3;
A104: y in Seg (len q9) by A102, FINSEQ_1:def 3;
reconsider y = y as Element of NAT by A102;
y <= n by A72, A104, FINSEQ_1:1;
then A105: y <= n + 1 by A101, XXREAL_0:2;
1 <= y by A104, FINSEQ_1:1;
then y in dom q by A71, A105, FINSEQ_3:25;
then q . y in rng q by FUNCT_1:def 3;
then q . y in A9 ;
hence x in A9 by A73, A102, A103; :: thesis:

end;

then reconsider f = q9 as FinSequence of A9 by FINSEQ_1:def 4, TARSKI:def 3;
dom q = Seg (n + 1) by A71, FINSEQ_1:def 3
.= Seg ((len q9) + (len <*x*>)) by A72, FINSEQ_1:39 ;
then A106: q9 ^ <*x*> = q by A73, A85, FINSEQ_1:def 7;
A107: not x in rng p

proof

(len p) + 1 = (len p) + (len <*x*>) by FINSEQ_1:39
.= len (p ^ <*x*>) by FINSEQ_1:22 ;
then (len p) + 1 in Seg (len (p ^ <*x*>)) by FINSEQ_1:4;
then A108: (len p) + 1 in dom (p ^ <*x*>) by FINSEQ_1:def 3;
assume x in rng p ; :: thesis:
then consider y being object such that
A109: y in dom p and
A110: x = p . y by FUNCT_1:def 3;
A111: y in Seg (len p) by A109, FINSEQ_1:def 3;
A112: dom p c= dom (p ^ <*x*>) by FINSEQ_1:26;
reconsider y = y as Element of NAT by A109;
x = (p ^ <*x*>) . y by A109, A110, FINSEQ_1:def 7;
then A113: x = (p ^ <*x*>) /. y by A109, A112, PARTFUN1:def 6;
y <= len p by A111, FINSEQ_1:1;
then A114: y < (len p) + 1 by NAT_1:13;
x = (p ^ <*x*>) . ((len p) + 1) by FINSEQ_1:42;
then (p ^ <*x*>) /. y = (p ^ <*x*>) /. ((len p) + 1) by A108, A113, PARTFUN1:def 6;
hence contradiction by A67, A109, A108, A112, A114; :: thesis:

end;

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

proof

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

proof

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

end;

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

end;

rng (p ^ <*x*>) = (rng p) \/ (rng <*x*>) by FINSEQ_1:31
.= (rng p) \/ {x} by FINSEQ_1:39 ;
then A120: rng p = (rng (p ^ <*x*>)) \ {x} by A115, TARSKI:2;
A121: ( 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

A122: not x in rng f

proof

(len f) + 1 = (len f) + (len <*x*>) by FINSEQ_1:39
.= len (f ^ <*x*>) by FINSEQ_1:22 ;
then (len f) + 1 in Seg (len (f ^ <*x*>)) by FINSEQ_1:4;
then A123: (len f) + 1 in dom (f ^ <*x*>) by FINSEQ_1:def 3;
assume x in rng f ; :: thesis:
then consider y being object such that
A124: y in dom f and
A125: x = f . y by FUNCT_1:def 3;
A126: y in Seg (len f) by A124, FINSEQ_1:def 3;
A127: dom f c= dom (f ^ <*x*>) by FINSEQ_1:26;
reconsider y = y as Element of NAT by A124;
x = q . y by A73, A124, A125;
then A128: x = q /. y by A106, A124, A127, PARTFUN1:def 6;
y <= len f by A126, FINSEQ_1:1;
then A129: y < (len f) + 1 by NAT_1:13;
x = q . ((len f) + 1) by A106, FINSEQ_1:42;
then q /. y = q /. ((len f) + 1) by A106, A123, A128, PARTFUN1:def 6;
hence contradiction by A69, A106, A124, A123, A127, A129; :: thesis:

end;

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

proof

let z be object ; :: thesis:

hereby :: thesis:

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

end;

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

end;

rng (f ^ <*x*>) = (rng f) \/ (rng <*x*>) by FINSEQ_1:31
.= (rng f) \/ {x} by FINSEQ_1:39 ;
hence rng f = rng p by A68, A106, A120, A130, TARSKI:2; :: thesis:
let l, m be Nat; :: thesis:
assume that
A135: l in dom f and
A136: m in dom f and
A137: l < m ; :: thesis:
A138: f . m = f /. m by A136, PARTFUN1:def 6;
A139: dom f c= dom q by A106, FINSEQ_1:26;
then q . m = q /. m by A136, PARTFUN1:def 6;
then A140: f /. m = q /. m by A73, A136, A138;
A141: f . l = f /. l by A135, PARTFUN1:def 6;
q . l = q /. l by A139, A135, PARTFUN1:def 6;
then f /. l = q /. l by A73, A135, A141;
hence ( f /. l <> f /. m & [(f /. l),(f /. m)] in R ) by A69, A139, A135, A136, A137, A140; :: 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
A142: l in dom p and
A143: m in dom p and
A144: l < m ; :: thesis:
A145: dom p c= dom (p ^ <*x*>) by FINSEQ_1:26;
p . m = (p ^ <*x*>) . m by A143, FINSEQ_1:def 7;
then p . m = (p ^ <*x*>) /. m by A143, A145, PARTFUN1:def 6;
then A146: p /. m = (p ^ <*x*>) /. m by A143, PARTFUN1:def 6;
p . l = (p ^ <*x*>) . l by A142, FINSEQ_1:def 7;
then p . l = (p ^ <*x*>) /. l by A142, A145, PARTFUN1:def 6;
then p /. l = (p ^ <*x*>) /. l by A142, PARTFUN1:def 6;
hence ( p /. l <> p /. m & [(p /. l),(p /. m)] in R ) by A67, A142, A143, A144, A145, A146; :: thesis:

end;

hence q = p ^ <*x*> by A66, A106, A121; :: thesis:

end;

A147: now :: thesis:

let n, m be Nat; :: thesis:
assume that
A148: n in dom p and
A149: m in dom p and
A150: n < m ; :: thesis:
A151: p /. m = p . m by A149, PARTFUN1:def 6
.= p9 /. m by A149, PARTFUN1:def 6 ;
p /. n = p . n by A148, PARTFUN1:def 6
.= p9 /. n by A148, PARTFUN1:def 6 ;
hence ( p /. n <> p /. m & [(p /. n),(p /. m)] in R ) by A60, A148, A149, A150, A151; :: thesis:

end;

A152: now :: thesis:

let n, m be Nat; :: thesis:
assume that
A153: n in dom q and
A154: m in dom q and
A155: n < m ; :: thesis:
A156: q /. m = q . m by A154, PARTFUN1:def 6
.= q9 /. m by A154, PARTFUN1:def 6 ;
q /. n = q . n by A153, PARTFUN1:def 6
.= q9 /. n by A153, PARTFUN1:def 6 ;
hence ( q /. n <> q /. m & [(q /. n),(q /. m)] in R ) by A62, A153, A154, A155, A156; :: thesis:

end;

A157: S₁[ <*> A9] ;
for p being FinSequence of A9 holds S₁[p] from FINSEQ_2:sch 2(A157, A65);
hence p9 = q9 by A59, A61, A147, A152; :: thesis:

end;