let p, q be FinSequence of NAT ; :: thesis:
assume A38: ( rng p = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len p & k1 = p . l & k2 = p . m holds
k1 < k2 ) & rng q = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len q & k1 = q . l & k2 = q . m holds
k1 < k2 ) ) ; :: thesis:
defpred S₂[ FinSequence] means for X being set st ex k being Nat st X c= Seg k & $1 is FinSequence of NAT & rng $1 = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len $1 & k1 = $1 . l & k2 = $1 . m holds
k1 < k2 ) holds
for q being FinSequence of NAT st rng q = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len q & k1 = q . l & k2 = q . m holds
k1 < k2 ) holds
q = $1;
A39: S₂[ {} ] ;
A40: for p being FinSequence
for x being set st S₂[p] holds
S₂[p ^ <*x*>]

let p be FinSequence; :: thesis:
let x be set ; :: thesis:
assume A41: S₂[p] ; :: thesis:
let X be set ; :: thesis:
given k being Nat such that A42: X c= Seg k ; :: thesis:
assume that
A43: p ^ <*x*> is FinSequence of NAT and
A44: rng (p ^ <*x*>) = X and
A45: for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len (p ^ <*x*>) & k1 = (p ^ <*x*>) . l & k2 = (p ^ <*x*>) . m holds
k1 < k2 ; :: thesis:
let q be FinSequence of NAT ; :: thesis:
assume that
A46: rng q = X and
A47: for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len q & k1 = q . l & k2 = q . m holds
k1 < k2 ; :: thesis:
1 in Seg 1 ;
then A48: 1 in dom <*x*> by Def8;
A49: ex m being Nat st
( m = x & ( for l being Nat st l in X & l <> x holds
l < m ) )

<*x*> is FinSequence of NAT by A43, Th50;
then rng <*x*> c= NAT by Def4;
then {x} c= NAT by Th55;
then reconsider m = x as Element of NAT by ZFMISC_1:37;
take m ; :: thesis:
thus m = x ; :: thesis:
thus for l being Nat st l in X & l <> x holds
l < m :: thesis:

proof

let l be Nat; :: thesis:
assume that
A50: l in X and
A51: l <> x ; :: thesis:
consider y being set such that
A52: y in dom (p ^ <*x*>) and
A53: l = (p ^ <*x*>) . y by A44, A50, FUNCT_1:def 5;
A54: y in Seg (len (p ^ <*x*>)) by A52, Def3;
reconsider k = y as Element of NAT by A52;
k <= len (p ^ <*x*>) by A54, Th3;
then k <= (len p) + (len <*x*>) by Th35;
then A55: k <= (len p) + 1 by Th56;
A56: k <> (len p) + 1

proof

assume k = (len p) + 1 ; :: thesis:
then (p ^ <*x*>) . k = <*x*> . 1 by A48, Def7
.= x by Def8 ;
hence contradiction by A51, A53; :: thesis:

end;

A57: 1 <= k by A54, Th3;
k < (len p) + 1 by A55, A56, XXREAL_0:1;
then k < (len p) + (len <*x*>) by Th56;
then A58: k < len (p ^ <*x*>) by Th35;
m = (p ^ <*x*>) . ((len p) + 1) by Th59
.= (p ^ <*x*>) . ((len p) + (len <*x*>)) by Th56
.= (p ^ <*x*>) . (len (p ^ <*x*>)) by Th35 ;
hence l < m by A45, A53, A57, A58; :: thesis:

end;

then reconsider m = x as Nat ;
len q <> 0

proof

assume len q = 0 ; :: thesis:
then p ^ <*x*> = {} by A44, A46, Lm4, RELAT_1:60;
then 0 = len (p ^ <*x*>)
.= (len p) + (len <*x*>) by Th35
.= 1 + (len p) by Th56 ;
hence contradiction ; :: thesis:

end;

then consider n being Nat such that
A59: len q = n + 1 by NAT_1:6;
deffunc H₁( Nat) -> set = q . $1;
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
A60: len q9 = n and
A61: for m being Nat st m in dom q9 holds
q9 . m = q . m ;

now

let x be set ; :: thesis:
assume x in rng q9 ; :: thesis:
then consider y being set such that
A62: y in dom q9 and
A63: x = q9 . y by FUNCT_1:def 5;
A64: y in Seg (len q9) by A62, Def3;
reconsider y = y as Element of NAT by A62;
A65: y <= n by A60, A64, Th3;
A66: n <= n + 1 by NAT_1:11;
A67: 1 <= y by A64, Th3;
y <= n + 1 by A65, A66, XXREAL_0:2;
then y in Seg (n + 1) by A67;
then y in dom q by A59, Def3;
then A68: q . y in rng q by FUNCT_1:def 5;
rng q c= NAT by Def4;
then q . y in NAT by A68;
hence x in NAT by A61, A62, A63; :: thesis:

end;

then rng q9 c= NAT by TARSKI:def 3;
then reconsider f = q9 as FinSequence of NAT by Def4;
A69: dom q = Seg (n + 1) by A59, Def3
.= Seg ((len q9) + (len <*x*>)) by A60, Th56 ;
A70: 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 A71: m in {1} by Def8, Th4;
then A72: m = 1 by TARSKI:def 1;
q . ((len q9) + m) = x

proof

assume q . ((len q9) + m) <> x ; :: thesis:
then A73: q . (len q) <> x by A59, A60, A71, TARSKI:def 1;
consider d being Nat such that
A74: d = x and
A75: for l being Nat st l in X & l <> x holds
l < d by A49;
x in {x} by TARSKI:def 1;
then x in rng <*x*> by Th55;
then x in (rng p) \/ (rng <*x*>) by XBOOLE_0:def 3;
then x in rng q by A44, A46, Th44;
then consider y being set such that
A76: y in dom q and
A77: x = q . y by FUNCT_1:def 5;
A78: y in Seg (len q) by A76, Def3;
reconsider y = y as Element of NAT by A76;
A79: 1 <= y by A78, Th3;
A80: y <= len q by A78, Th3;
then A81: y < len q by A73, A77, XXREAL_0:1;
A82: rng q c= NAT by Def4;
1 <= len q by A79, A80, XXREAL_0:2;
then len q in Seg (len q) ;
then A83: len q in dom q by Def3;
then A84: q . (len q) in rng q by FUNCT_1:def 5;
A85: q . (len q) in X by A46, A83, FUNCT_1:def 5;
reconsider k = q . (len q) as Nat by A82, A84;
k < d by A73, A75, A85;
hence contradiction by A47, A74, A77, A79, A81; :: thesis:

end;

hence q . ((len q9) + m) = <*x*> . m by A72, Th57; :: thesis:

end;

then A86: q9 ^ <*x*> = q by A61, A69, Def7;
A87: ex m being Nat st X \ {x} c= Seg m by A42, XBOOLE_1:1;
A88: not x in rng p

proof

assume x in rng p ; :: thesis:
then consider y being set such that
A89: y in dom p and
A90: x = p . y by FUNCT_1:def 5;
A91: y in Seg (len p) by A89, Def3;
reconsider y = y as Element of NAT by A89;
A92: y <= len p by A91, Th3;
A93: (len p) + 1 = (len p) + (len <*x*>) by Th56
.= len (p ^ <*x*>) by Th35 ;
A94: 1 <= y by A91, Th3;
A95: y < (len p) + 1 by A92, NAT_1:13;
A96: m = (p ^ <*x*>) . y by A89, A90, Def7;
m = (p ^ <*x*>) . ((len p) + 1) by Th59;
hence contradiction by A45, A93, A94, A95, A96; :: thesis:

end;

A97: X = (rng p) \/ (rng <*x*>) by A44, Th44
.= (rng p) \/ {x} by Th56 ;
A98: 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 A99: z in ((rng p) \/ {x}) \ {x} ; :: thesis:
then not z in {x} by XBOOLE_0:def 5;
hence z in rng p by A99, XBOOLE_0:def 3; :: thesis:

end;

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

end;

A100: for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len p & k1 = p . l & k2 = p . m holds
k1 < k2

proof

let l, m, k1, k2 be Nat; :: thesis:
assume that
A101: 1 <= l and
A102: l < m and
A103: m <= len p and
A104: k1 = p . l and
A105: k2 = p . m ; :: thesis:
l <= len p by A102, A103, XXREAL_0:2;
then l in Seg (len p) by A101, Th3;
then l in dom p by Def3;
then A106: k1 = (p ^ <*x*>) . l by A104, Def7;
1 <= m by A101, A102, XXREAL_0:2;
then m in Seg (len p) by A103, Th3;
then m in dom p by Def3;
then A107: k2 = (p ^ <*x*>) . m by A105, Def7;
len p <= (len p) + 1 by NAT_1:11;
then m <= (len p) + 1 by A103, XXREAL_0:2;
then m <= (len p) + (len <*x*>) by Th56;
then m <= len (p ^ <*x*>) by Th35;
hence k1 < k2 by A45, A101, A102, A106, A107; :: thesis:

end;

A108: p is FinSequence of NAT by A43, Th50;
A109: rng p = X \ {x} by A97, A98, TARSKI:2;
A110: not x in rng f

proof

assume x in rng f ; :: thesis:
then consider y being set such that
A111: y in dom f and
A112: x = f . y by FUNCT_1:def 5;
A113: y in Seg (len f) by A111, Def3;
reconsider y = y as Element of NAT by A111;
A114: y <= len f by A113, Th3;
A115: (len f) + 1 = (len f) + (len <*x*>) by Th56
.= len (f ^ <*x*>) by Th35 ;
A116: 1 <= y by A113, Th3;
A117: y < (len f) + 1 by A114, NAT_1:13;
A118: m = q . y by A61, A111, A112;
m = q . ((len f) + 1) by A86, Th59;
hence contradiction by A47, A86, A115, A116, A117, A118; :: thesis:

end;

A119: X = (rng f) \/ (rng <*x*>) by A46, A86, Th44
.= (rng f) \/ {x} by Th56 ;
A120: for z being set holds
( z in ((rng f) \/ {x}) \ {x} iff z in rng f )

proof

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

proof

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

end;

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

end;

A122: for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len f & k1 = f . l & k2 = f . m holds
k1 < k2

proof

let l, m, k1, k2 be Nat; :: thesis:
assume that
A123: 1 <= l and
A124: l < m and
A125: m <= len f and
A126: k1 = f . l and
A127: k2 = f . m ; :: thesis:
A128: m <= len q by A59, A60, A125, NAT_1:13;
l <= n by A60, A124, A125, XXREAL_0:2;
then A129: l in Seg n by A123, Th3;
1 <= m by A123, A124, XXREAL_0:2;
then A130: m in Seg n by A60, A125, Th3;
A131: l in dom q9 by A60, A129, Def3;
A132: m in dom q9 by A60, A130, Def3;
A133: k1 = q . l by A61, A126, A131;
k2 = q . m by A61, A127, A132;
hence k1 < k2 by A47, A123, A124, A128, A133; :: thesis:

end;

rng f = X \ {x} by A119, A120, TARSKI:2;
then q9 = p by A41, A87, A100, A108, A109, A122;
hence q = p ^ <*x*> by A61, A69, A70, Def7; :: thesis:

end;

for p being FinSequence holds S₂[p] from FINSEQ_1:sch 3(A39, A40);
hence p = q by A1, A38; :: thesis: