let p, q be FinSequence of NAT ; ( 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 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 ) )
; p = q
defpred S2[ 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:
S2[ {} ]
;
A39:
for p being FinSequence
for x being object st S2[p] holds
S2[p ^ <*x*>]
proof
let p be
FinSequence;
for x being object st S2[p] holds
S2[p ^ <*x*>]let x be
object ;
( S2[p] implies S2[p ^ <*x*>] )
assume A40:
S2[
p]
;
S2[p ^ <*x*>]
let X be
set ;
( 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 A41:
X c= Seg k
;
( 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 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
;
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 ;
( 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 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
;
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
;
( m = x & ( for l being Nat st l in X & l <> x holds
l < m ) )
thus
m = x
;
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
verumproof
let l be
Nat;
( l in X & l <> x implies l < m )
assume that A49:
l in X
and A50:
l <> x
;
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
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;
verum
end;
end;
then reconsider m =
x as
Nat ;
len q <> 0
then consider n being
Nat such that A58:
len q = n + 1
by NAT_1:6;
deffunc H1(
Nat)
-> set =
q . $1;
ex
q9 being
FinSequence st
(
len q9 = n & ( for
m being
Nat st
m in dom q9 holds
q9 . m = H1(
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
;
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;
( m in dom <*x*> implies q . ((len q9) + m) = <*x*> . m )
assume
m in dom <*x*>
;
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
;
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;
verum
end;
hence
q . ((len q9) + m) = <*x*> . m
by A71, Th40;
verum
end;
then A83:
q9 ^ <*x*> = q
by A60, A68, Def7;
A84:
not
x in rng p
proof
assume
x in rng p
;
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;
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 )
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;
( 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
;
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;
verum
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
;
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;
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 )
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;
( 1 <= l & l < m & m <= len f & k1 = f . l & k2 = f . m implies k1 < k2 )
assume that A119:
1
<= l
and A120:
l < m
and A121:
m <= len f
and A122:
k1 = f . l
and A123:
k2 = f . m
;
k1 < k2
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;
verum
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;
verum
end;
for p being FinSequence holds S2[p]
from FINSEQ_1:sch 3(A38, A39);
hence
p = q
by A1, A37; verum