let p, q be FinSequence of NAT ; :: thesis:
assume A37: ( 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;
A38: S₂[ {} ] ;
A39: for p being FinSequence
for x being object st S₂[p] holds
S₂[p ^ <*x*>]

let p be FinSequence; :: thesis:
let x be object ; :: thesis:
assume A40: S₂[p] ; :: thesis:
let X be set ; :: thesis:
given k being Nat such that A41: X c= Seg k ; :: thesis:
assume that
A42: p ^ <*x*> is FinSequence of NAT and
A43: rng (p ^ <*x*>) = X and
A44: 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
A45: rng q = X and
A46: 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 A47: 1 in dom <*x*> by Def8;
A48: 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 A42, Th36;
then rng <*x*> c= NAT by Def4;
then {x} c= NAT by Th38;
then reconsider m = x as Element of NAT by ZFMISC_1:31;
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
A49: l in X and
A50: l <> x ; :: thesis:
consider y being object such that
A51: y in dom (p ^ <*x*>) and
A52: l = (p ^ <*x*>) . y by A43, A49, FUNCT_1:def 3;
A53: y in Seg (len (p ^ <*x*>)) by A51, Def3;
reconsider k = y as Element of NAT by A51;
k <= len (p ^ <*x*>) by A53, Th1;
then k <= (len p) + (len <*x*>) by Th22;
then A54: k <= (len p) + 1 by Th39;
A55: k <> (len p) + 1

proof

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

end;

A56: 1 <= k by A53, Th1;
k < (len p) + 1 by A54, A55, XXREAL_0:1;
then k < (len p) + (len <*x*>) by Th39;
then A57: k < len (p ^ <*x*>) by Th22;
m = (p ^ <*x*>) . ((len p) + 1) by Th42
.= (p ^ <*x*>) . ((len p) + (len <*x*>)) by Th39
.= (p ^ <*x*>) . (len (p ^ <*x*>)) by Th22 ;
hence l < m by A44, A52, A56, A57; :: thesis:

end;

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

proof

assume len q = 0 ; :: thesis:
then p ^ <*x*> = {} by A43, A45, Lm3, RELAT_1:38;
then 0 = len (p ^ <*x*>)
.= (len p) + (len <*x*>) by Th22
.= 1 + (len p) by Th39 ;
hence contradiction ; :: thesis:

end;

then consider n being Nat such that
A58: 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
A59: len q9 = n and
A60: for m being Nat st m in dom q9 holds
q9 . m = q . m ;

now :: thesis:

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

end;

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

proof

assume q . ((len q9) + m) <> x ; :: thesis:
then A72: q . (len q) <> x by A58, A59, A70, TARSKI:def 1;
consider d being Nat such that
A73: d = x and
A74: for l being Nat st l in X & l <> x holds
l < d by A48;
x in {x} by TARSKI:def 1;
then x in rng <*x*> by Th38;
then x in (rng p) \/ (rng <*x*>) by XBOOLE_0:def 3;
then x in rng q by A43, A45, Th31;
then consider y being object such that
A75: y in dom q and
A76: x = q . y by FUNCT_1:def 3;
A77: y in Seg (len q) by A75, Def3;
reconsider y = y as Element of NAT by A75;
A78: 1 <= y by A77, Th1;
A79: y <= len q by A77, Th1;
then A80: y < len q by A72, A76, XXREAL_0:1;
1 <= len q by A78, A79, XXREAL_0:2;
then len q in Seg (len q) ;
then A81: len q in dom q by Def3;
A82: q . (len q) in X by A45, A81, FUNCT_1:def 3;
reconsider k = q . (len q) as Nat ;
k < d by A72, A74, A82;
hence contradiction by A46, A73, A76, A78, A80; :: thesis:

end;

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

end;

then A83: q9 ^ <*x*> = q by A60, A68, Def7;
A84: not x in rng p

proof

assume x in rng p ; :: thesis:
then consider y being object such that
A85: y in dom p and
A86: x = p . y by FUNCT_1:def 3;
A87: y in Seg (len p) by A85, Def3;
reconsider y = y as Element of NAT by A85;
A88: y <= len p by A87, Th1;
A89: (len p) + 1 = (len p) + (len <*x*>) by Th39
.= len (p ^ <*x*>) by Th22 ;
A90: 1 <= y by A87, Th1;
A91: y < (len p) + 1 by A88, NAT_1:13;
A92: m = (p ^ <*x*>) . y by A85, A86, Def7;
m = (p ^ <*x*>) . ((len p) + 1) by Th42;
hence contradiction by A44, A89, A90, A91, A92; :: thesis:

end;

A93: X = (rng p) \/ (rng <*x*>) by A43, Th31
.= (rng p) \/ {x} by Th39 ;
A94: 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 A95: z in ((rng p) \/ {x}) \ {x} ; :: thesis:
then not z in {x} by XBOOLE_0:def 5;
hence z in rng p by A95, XBOOLE_0:def 3; :: thesis:

end;

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

end;

A96: 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
A97: 1 <= l and
A98: l < m and
A99: m <= len p and
A100: k1 = p . l and
A101: k2 = p . m ; :: thesis:
l <= len p by A98, A99, XXREAL_0:2;
then l in Seg (len p) by A97;
then l in dom p by Def3;
then A102: k1 = (p ^ <*x*>) . l by A100, Def7;
1 <= m by A97, A98, XXREAL_0:2;
then m in Seg (len p) by A99;
then m in dom p by Def3;
then A103: k2 = (p ^ <*x*>) . m by A101, Def7;
len p <= (len p) + 1 by NAT_1:11;
then m <= (len p) + 1 by A99, XXREAL_0:2;
then m <= (len p) + (len <*x*>) by Th39;
then m <= len (p ^ <*x*>) by Th22;
hence k1 < k2 by A44, A97, A98, A102, A103; :: thesis:

end;

A104: p is FinSequence of NAT by A42, Th36;
A105: rng p = X \ {x} by A93, A94, TARSKI:2;
A106: not x in rng f

proof

assume x in rng f ; :: thesis:
then consider y being object such that
A107: y in dom f and
A108: x = f . y by FUNCT_1:def 3;
A109: y in Seg (len f) by A107, Def3;
reconsider y = y as Element of NAT by A107;
A110: y <= len f by A109, Th1;
A111: (len f) + 1 = (len f) + (len <*x*>) by Th39
.= len (f ^ <*x*>) by Th22 ;
A112: 1 <= y by A109, Th1;
A113: y < (len f) + 1 by A110, NAT_1:13;
A114: m = q . y by A60, A107, A108;
m = q . ((len f) + 1) by A83, Th42;
hence contradiction by A46, A83, A111, A112, A113, A114; :: thesis:

end;

A115: X = (rng f) \/ (rng <*x*>) by A45, A83, Th31
.= (rng f) \/ {x} by Th39 ;
A116: for z being object holds
( z in ((rng f) \/ {x}) \ {x} iff z in rng f )

proof

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

proof

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

end;

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

end;

A118: 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
A119: 1 <= l and
A120: l < m and
A121: m <= len f and
A122: k1 = f . l and
A123: k2 = f . m ; :: thesis:
A124: m <= len q by A58, A59, A121, NAT_1:13;
l <= n by A59, A120, A121, XXREAL_0:2;
then A125: l in Seg n by A119;
1 <= m by A119, A120, XXREAL_0:2;
then A126: m in Seg n by A59, A121;
A127: l in dom q9 by A59, A125, Def3;
A128: m in dom q9 by A59, A126, Def3;
A129: k1 = q . l by A60, A122, A127;
k2 = q . m by A60, A123, A128;
hence k1 < k2 by A46, A119, A120, A124, A129; :: thesis:

end;

rng f = X \ {x} by A115, A116, TARSKI:2;
then q9 = p by A40, A41, A96, A104, A105, A118, XBOOLE_1:1;
hence q = p ^ <*x*> by A60, A68, A69, Def7; :: thesis:

end;

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