let p, q be FinSequence of NAT ; :: thesis: ( 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 ) implies p = q )
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: p = q
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*>]

proof

let p be FinSequence; :: thesis: for x being set st S₂[p] holds
S₂[p ^ <*x*>]
let x be set ; :: thesis: ( S₂[p] implies S₂[p ^ <*x*>] )
assume A41: S₂[p] ; :: thesis: S₂[p ^ <*x*>]
let X be set ; :: thesis: ( ex k being Nat st X c= Seg k & p ^ <*x*> is FinSequence of NAT & rng (p ^ <*x*>) = X & ( 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 ) implies 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 = p ^ <*x*> )
given k being Nat such that A42: X c= Seg k ; :: thesis: ( not p ^ <*x*> is FinSequence of NAT or not rng (p ^ <*x*>) = X or ex l, m, k1, k2 being Nat st
( 1 <= l & l < m & m <= len (p ^ <*x*>) & k1 = (p ^ <*x*>) . l & k2 = (p ^ <*x*>) . m & not k1 < k2 ) or 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 = p ^ <*x*> )
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: 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 = p ^ <*x*>
let q be FinSequence of NAT ; :: thesis: ( 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 ) implies q = p ^ <*x*> )
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: q = p ^ <*x*>
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 ) )

proof

<*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:31;
take m ; :: thesis: ( m = x & ( for l being Nat st l in X & l <> x holds
l < m ) )
thus m = x ; :: thesis: for l being Nat st l in X & l <> x holds
l < m
thus for l being Nat st l in X & l <> x holds
l < m :: thesis: verum

proof

let l be Nat; :: thesis: ( l in X & l <> x implies l < m )
assume that
A50: l in X and
A51: l <> x ; :: thesis: l < m
consider y being set such that
A52: y in dom (p ^ <*x*>) and
A53: l = (p ^ <*x*>) . y by A44, A50, FUNCT_1:def 3;
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: contradiction
then (p ^ <*x*>) . k = <*x*> . 1 by A48, Def7
.= x by Def8 ;
hence contradiction by A51, A53; :: thesis: verum

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: verum

end;

end;

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

proof

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

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: ( x in rng q9 implies x in NAT )
assume x in rng q9 ; :: thesis: x in NAT
then consider y being set such that
A62: y in dom q9 and
A63: x = q9 . y by FUNCT_1:def 3;
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 3;
rng q c= NAT by Def4;
then q . y in NAT by A68;
hence x in NAT by A61, A62, A63; :: thesis: verum

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: ( m in dom <*x*> implies q . ((len q9) + m) = <*x*> . m )
assume m in dom <*x*> ; :: thesis: q . ((len q9) + m) = <*x*> . m
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: contradiction
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 3;
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;
1 <= len q by A79, A80, XXREAL_0:2;
then len q in Seg (len q) ;
then A82: len q in dom q by Def3;
A83: q . (len q) in X by A46, A82, FUNCT_1:def 3;
reconsider k = q . (len q) as Nat ;
k < d by A73, A75, A83;
hence contradiction by A47, A74, A77, A79, A81; :: thesis: verum

end;

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

end;

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

proof

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

end;

A95: X = (rng p) \/ (rng <*x*>) by A44, Th44
.= (rng p) \/ {x} by Th56 ;
A96: for z being set holds
( z in ((rng p) \/ {x}) \ {x} iff z in rng p )

proof

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

proof

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

end;

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

end;

A98: 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: ( 1 <= l & l < m & m <= len p & k1 = p . l & k2 = p . m implies k1 < k2 )
assume that
A99: 1 <= l and
A100: l < m and
A101: m <= len p and
A102: k1 = p . l and
A103: k2 = p . m ; :: thesis: k1 < k2
l <= len p by A100, A101, XXREAL_0:2;
then l in Seg (len p) by A99, Th3;
then l in dom p by Def3;
then A104: k1 = (p ^ <*x*>) . l by A102, Def7;
1 <= m by A99, A100, XXREAL_0:2;
then m in Seg (len p) by A101, Th3;
then m in dom p by Def3;
then A105: k2 = (p ^ <*x*>) . m by A103, Def7;
len p <= (len p) + 1 by NAT_1:11;
then m <= (len p) + 1 by A101, XXREAL_0:2;
then m <= (len p) + (len <*x*>) by Th56;
then m <= len (p ^ <*x*>) by Th35;
hence k1 < k2 by A45, A99, A100, A104, A105; :: thesis: verum

end;

A106: p is FinSequence of NAT by A43, Th50;
A107: rng p = X \ {x} by A95, A96, TARSKI:1;
A108: not x in rng f

proof

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

end;

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

proof

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

proof

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

end;

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

end;

A120: 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: ( 1 <= l & l < m & m <= len f & k1 = f . l & k2 = f . m implies k1 < k2 )
assume that
A121: 1 <= l and
A122: l < m and
A123: m <= len f and
A124: k1 = f . l and
A125: k2 = f . m ; :: thesis: k1 < k2
A126: m <= len q by A59, A60, A123, NAT_1:13;
l <= n by A60, A122, A123, XXREAL_0:2;
then A127: l in Seg n by A121, Th3;
1 <= m by A121, A122, XXREAL_0:2;
then A128: m in Seg n by A60, A123, Th3;
A129: l in dom q9 by A60, A127, Def3;
A130: m in dom q9 by A60, A128, Def3;
A131: k1 = q . l by A61, A124, A129;
k2 = q . m by A61, A125, A130;
hence k1 < k2 by A47, A121, A122, A126, A131; :: thesis: verum

end;

rng f = X \ {x} by A117, A118, TARSKI:1;
then q9 = p by A41, A85, A98, A106, A107, A120;
hence q = p ^ <*x*> by A61, A69, A70, Def7; :: thesis: verum

end;

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