let p, q be FinSequence of NAT ; :: thesis: ( rng p = X & ( for m, n being Nat st 1 <= m & m < n & n <= len p holds
p . m < p . n ) & rng q = X & ( for m, n being Nat st 1 <= m & m < n & n <= len q holds
q . m < q . n ) implies p = q )
assume that
A37: rng p = X and
g01: for l, m being Nat st 1 <= l & l < m & m <= len p holds
p . l < p . m and
g02: rng q = X and
g03: for l, m being Nat st 1 <= l & l < m & m <= len q holds
q . l < q . m ; :: thesis: p = q
a37: for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len p & k1 = p . l & k2 = p . m holds
k1 < k2 by g01;
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 being Nat st 1 <= l & l < m & m <= len q holds
q . l < q . m ) holds
q = $1;
A38: S₂[ {} ] ;
A39: for p being FinSequence
for x being object st S₂[p] holds
S₂[p ^ <*x*>]

proof

let p be FinSequence; :: thesis: for x being object st S₂[p] holds
S₂[p ^ <*x*>]
let x be object ; :: thesis: ( S₂[p] implies S₂[p ^ <*x*>] )
assume A40: 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 being Nat st 1 <= l & l < m & m <= len q holds
q . l < q . m ) holds
q = p ^ <*x*> )
given k being Nat such that A41: 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 being Nat st 1 <= l & l < m & m <= len q holds
q . l < q . m ) holds
q = p ^ <*x*> )
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: for q being FinSequence of NAT st rng q = X & ( for l, m being Nat st 1 <= l & l < m & m <= len q holds
q . l < q . m ) holds
q = p ^ <*x*>
reconsider p = p as FinSequence of NAT by A42, Th36;
let q be FinSequence of NAT ; :: thesis: ( rng q = X & ( for l, m being Nat st 1 <= l & l < m & m <= len q holds
q . l < q . m ) implies q = p ^ <*x*> )
assume that
A45: rng q = X and
A46: for l, m being Nat st 1 <= l & l < m & m <= len q holds
q . l < q . m ; :: thesis: q = p ^ <*x*>
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 ) )

proof

<*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: ( 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
A49: l in X and
A50: l <> x ; :: thesis: l < m
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: contradiction
then (p ^ <*x*>) . k = <*x*> . 1 by A47, Def7
.= x ;
hence contradiction by A50, A52; :: thesis: verum

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

end;

end;

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

proof

assume len q = 0 ; :: thesis: contradiction
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: verum

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: for x being object st x in rng q9 holds
x in NAT

let x be object ; :: thesis: ( x in rng q9 implies x in NAT )
assume x in rng q9 ; :: thesis: x in NAT
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: verum

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: ( m in dom <*x*> implies q . ((len q9) + m) = <*x*> . m )
assume m in dom <*x*> ; :: thesis: q . ((len q9) + m) = <*x*> . m
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: contradiction
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: verum

end;

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

end;

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

proof

assume x in rng p ; :: thesis: contradiction
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: verum

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: ( 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 A95: 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 A95, 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 A84, TARSKI:def 1, XBOOLE_0:def 3;
hence z in ((rng p) \/ {x}) \ {x} by XBOOLE_0:def 5; :: thesis: verum

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: ( 1 <= l & l < m & m <= len p & k1 = p . l & k2 = p . m implies k1 < k2 )
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: k1 < k2
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: verum

end;

A105: rng p = X \ {x} by A93, A94, TARSKI:2;
A106: not x in rng f

proof

assume x in rng f ; :: thesis: contradiction
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: verum

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: ( 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 A117: 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 A117, 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 A106, TARSKI:def 1, XBOOLE_0:def 3;
hence z in ((rng f) \/ {x}) \ {x} by XBOOLE_0:def 5; :: thesis: verum

end;

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

proof

let l, m be Nat; :: thesis: ( 1 <= l & l < m & m <= len f implies f . l < f . m )
assume that
A119: 1 <= l and
A120: l < m and
A121: m <= len f ; :: thesis: f . l < f . m
set k1 = f . l;
set k2 = f . m;
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: f . l = q . l by A60, A127;
f . m = q . m by A60, A128;
hence f . l < f . m by A46, A119, A120, A124, A129; :: thesis: verum

end;

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

end;

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