defpred S1[ XFinSequence] means for X being set st ex k being Nat st X c= k & $1 is XFinSequence of NAT & rng $1 = X & ( for l, m, k1, k2 being Nat st l < m & m < len $1 & k1 = $1 . l & k2 = $1 . m holds
k1 < k2 ) holds
for q being XFinSequence of NAT st rng q = X & ( for l, m, k1, k2 being Nat st l < m & m < len q & k1 = q . l & k2 = q . m holds
k1 < k2 ) holds
q = $1;
let p, q be XFinSequence of NAT ; ( rng p = X & ( for l, m, k1, k2 being Nat st 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 l < m & m < len q & k1 = q . l & k2 = q . m holds
k1 < k2 ) implies p = q )
assume that
A31:
rng p = X
and
A32:
for l, m, k1, k2 being Nat st l < m & m < len p & k1 = p . l & k2 = p . m holds
k1 < k2
and
A33:
rng q = X
and
A34:
for l, m, k1, k2 being Nat st l < m & m < len q & k1 = q . l & k2 = q . m holds
k1 < k2
; p = q
A35:
for p being XFinSequence
for x being object st S1[p] holds
S1[p ^ <%x%>]
proof
let p be
XFinSequence;
for x being object st S1[p] holds
S1[p ^ <%x%>]let x be
object ;
( S1[p] implies S1[p ^ <%x%>] )
assume A36:
S1[
p]
;
S1[p ^ <%x%>]
let X be
set ;
( ex k being Nat st X c= k & p ^ <%x%> is XFinSequence of NAT & rng (p ^ <%x%>) = X & ( for l, m, k1, k2 being Nat st l < m & m < len (p ^ <%x%>) & k1 = (p ^ <%x%>) . l & k2 = (p ^ <%x%>) . m holds
k1 < k2 ) implies for q being XFinSequence of NAT st rng q = X & ( for l, m, k1, k2 being Nat st l < m & m < len q & k1 = q . l & k2 = q . m holds
k1 < k2 ) holds
q = p ^ <%x%> )
given k being
Nat such that A37:
X c= k
;
( not p ^ <%x%> is XFinSequence of NAT or not rng (p ^ <%x%>) = X or ex l, m, k1, k2 being Nat st
( l < m & m < len (p ^ <%x%>) & k1 = (p ^ <%x%>) . l & k2 = (p ^ <%x%>) . m & not k1 < k2 ) or for q being XFinSequence of NAT st rng q = X & ( for l, m, k1, k2 being Nat st l < m & m < len q & k1 = q . l & k2 = q . m holds
k1 < k2 ) holds
q = p ^ <%x%> )
assume that A38:
p ^ <%x%> is
XFinSequence of
NAT
and A39:
rng (p ^ <%x%>) = X
and A40:
for
l,
m,
k1,
k2 being
Nat st
l < m &
m < len (p ^ <%x%>) &
k1 = (p ^ <%x%>) . l &
k2 = (p ^ <%x%>) . m holds
k1 < k2
;
for q being XFinSequence of NAT st rng q = X & ( for l, m, k1, k2 being Nat st l < m & m < len q & k1 = q . l & k2 = q . m holds
k1 < k2 ) holds
q = p ^ <%x%>
let q be
XFinSequence of
NAT ;
( rng q = X & ( for l, m, k1, k2 being Nat st l < m & m < len q & k1 = q . l & k2 = q . m holds
k1 < k2 ) implies q = p ^ <%x%> )
assume that A41:
rng q = X
and A42:
for
l,
m,
k1,
k2 being
Nat st
l < m &
m < len q &
k1 = q . l &
k2 = q . m holds
k1 < k2
;
q = p ^ <%x%>
deffunc H1(
Nat)
-> Element of
omega =
q . $1;
len q <> 0
then consider n being
Nat such that A43:
len q = n + 1
by NAT_1:6;
A44:
ex
m being
Nat st
(
m = x & ( for
l being
Nat st
l in X &
l <> x holds
l < m ) )
proof
<%x%> is
XFinSequence of
NAT
by A38, AFINSQ_1:31;
then
rng <%x%> c= NAT
by RELAT_1:def 19;
then
{x} c= NAT
by AFINSQ_1:33;
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
len <%x%> = 1
by AFINSQ_1:34;
then A45:
m =
(p ^ <%x%>) . (((len p) + (len <%x%>)) - 1)
by AFINSQ_1:36
.=
(p ^ <%x%>) . ((len (p ^ <%x%>)) - 1)
by AFINSQ_1:17
;
len (p ^ <%x%>) < (len (p ^ <%x%>)) + 1
by XREAL_1:29;
then A46:
(len (p ^ <%x%>)) - 1
< len (p ^ <%x%>)
by XREAL_1:19;
let l be
Nat;
( l in X & l <> x implies l < m )
assume that A47:
l in X
and A48:
l <> x
;
l < m
consider y being
object such that A49:
y in dom (p ^ <%x%>)
and A50:
l = (p ^ <%x%>) . y
by A39, A47, FUNCT_1:def 3;
reconsider k =
y as
Element of
NAT by A49;
k < len (p ^ <%x%>)
by A49, AFINSQ_1:86;
then
k < (len p) + (len <%x%>)
by AFINSQ_1:17;
then
k < (len p) + 1
by AFINSQ_1:34;
then A51:
k <= len p
by NAT_1:13;
k <> len p
by A48, A50, AFINSQ_1:36;
then
k < ((len p) + 1) - 1
by A51, XXREAL_0:1;
then
k < ((len p) + (len <%x%>)) - 1
by AFINSQ_1:34;
then A52:
k < (len (p ^ <%x%>)) - 1
by AFINSQ_1:17;
then
(len (p ^ <%x%>)) -' 1
= (len (p ^ <%x%>)) - 1
by XREAL_0:def 2;
hence
l < m
by A40, A50, A52, A46, A45;
verum
end;
end;
then reconsider m =
x as
Nat ;
A53:
not
x in rng p
A59:
for
z being
object holds
(
z in ((rng p) \/ {x}) \ {x} iff
z in rng p )
deffunc H2(
set )
-> Element of
omega =
q . $1;
consider q9 being
XFinSequence such that A63:
len q9 = n
and A64:
for
m being
Nat st
m in n holds
q9 . m = H2(
m)
from AFINSQ_1:sch 2();
then
rng q9 c= NAT
;
then reconsider f =
q9 as
XFinSequence of
NAT by RELAT_1:def 19;
A67:
p is
XFinSequence of
NAT
by A38, AFINSQ_1:31;
A68:
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
m in len <%x%>
;
then A69:
m in 1
by AFINSQ_1:34;
Segm (0 + 1) = (Segm 0) \/ {0}
by AFINSQ_1:2;
then A70:
m = 0
by A69, TARSKI:def 1;
q . ((len q9) + m) = x
proof
x in {x}
by TARSKI:def 1;
then
x in rng <%x%>
by AFINSQ_1:33;
then
x in (rng p) \/ (rng <%x%>)
by XBOOLE_0:def 3;
then
x in rng q
by A39, A41, AFINSQ_1:26;
then consider y being
object such that A71:
y in dom q
and A72:
x = q . y
by FUNCT_1:def 3;
reconsider y =
y as
Element of
NAT by A71;
y + 1
<= len q
by NAT_1:13, A71, AFINSQ_1:86;
then A73:
y <= (len q) - 1
by XREAL_1:19;
len q < (len q) + 1
by XREAL_1:29;
then
(len q) - 1
in dom q
by A43, AFINSQ_1:86, XREAL_1:19;
then A74:
q . ((len q) - 1) in X
by A41, FUNCT_1:def 3;
len q < (len q) + 1
by XREAL_1:29;
then A75:
( (
y < (len q) - 1 &
(len q) - 1
< len q ) or
y = (len q) - 1 )
by A73, XREAL_1:19, XXREAL_0:1;
set k =
q . ((len q) - 1);
consider d being
Nat such that A76:
d = x
and A77:
for
l being
Nat st
l in X &
l <> x holds
l < d
by A44;
assume
q . ((len q9) + m) <> x
;
contradiction
then
q . ((len q) - 1) < d
by A43, A63, A70, A77, A74;
hence
contradiction
by A42, A43, A76, A72, A75;
verum
end;
hence
q . ((len q9) + m) = <%x%> . m
by A70;
verum
end;
A78:
dom q = (len q9) + (len <%x%>)
by A43, A63, AFINSQ_1:34;
then A79:
q9 ^ <%x%> = q
by A63, A64, A68, AFINSQ_1:def 3;
A80:
not
x in rng f
A86:
for
z being
object holds
(
z in ((rng f) \/ {x}) \ {x} iff
z in rng f )
X =
(rng p) \/ (rng <%x%>)
by A39, AFINSQ_1:26
.=
(rng p) \/ {x}
by AFINSQ_1:33
;
then A90:
rng p = X \ {x}
by A59, TARSKI:2;
A91:
for
l,
m,
k1,
k2 being
Nat st
l < m &
m < len p &
k1 = p . l &
k2 = p . m holds
k1 < k2
proof
let l,
m,
k1,
k2 be
Nat;
( l < m & m < len p & k1 = p . l & k2 = p . m implies k1 < k2 )
assume that A92:
l < m
and A93:
m < len p
and A94:
k1 = p . l
and A95:
k2 = p . m
;
k1 < k2
l < len p
by A92, A93, XXREAL_0:2;
then
l in dom p
by AFINSQ_1:86;
then A96:
k1 = (p ^ <%x%>) . l
by A94, AFINSQ_1:def 3;
len p < (len p) + 1
by XREAL_1:29;
then
m < (len p) + 1
by A93, XXREAL_0:2;
then
m < (len p) + (len <%x%>)
by AFINSQ_1:34;
then A97:
m < len (p ^ <%x%>)
by AFINSQ_1:17;
m in dom p
by A93, AFINSQ_1:86;
then
k2 = (p ^ <%x%>) . m
by A95, AFINSQ_1:def 3;
hence
k1 < k2
by A40, A92, A96, A97;
verum
end;
A98:
for
l,
m,
k1,
k2 being
Nat st
l < m &
m < len f &
k1 = f . l &
k2 = f . m holds
k1 < k2
proof
let l,
m,
k1,
k2 be
Nat;
( l < m & m < len f & k1 = f . l & k2 = f . m implies k1 < k2 )
assume that A99:
l < m
and A100:
m < len f
and A101:
k1 = f . l
and A102:
k2 = f . m
;
k1 < k2
A103:
k2 = q . m
by A64, A102, A63, A100, AFINSQ_1:86;
l < n
by A63, A99, A100, XXREAL_0:2;
then
l in Segm n
by NAT_1:44;
then A104:
k1 = q . l
by A64, A101;
m < len q
by A43, A63, A100, NAT_1:13;
hence
k1 < k2
by A42, A99, A104, A103;
verum
end;
X =
(rng f) \/ (rng <%x%>)
by A41, A79, AFINSQ_1:26
.=
(rng f) \/ {x}
by AFINSQ_1:33
;
then A105:
rng f = X \ {x}
by A86, TARSKI:2;
ex
m being
Nat st
X \ {x} c= m
by A37, XBOOLE_1:1;
then
q9 = p
by A36, A91, A67, A90, A98, A105;
hence
q = p ^ <%x%>
by A63, A64, A78, A68, AFINSQ_1:def 3;
verum
end;
A106:
S1[ {} ]
;
A107:
for p being XFinSequence holds S1[p]
from AFINSQ_1:sch 3(A106, A35);
ex k being Nat st X c= Segm k
by Th2;
hence
p = q
by A31, A32, A33, A34, A107; verum