reconsider IT = { <*k*> where k is Element of NAT : k < n } \/ {{} } as non empty set ;
A1:
IT is Tree-like
proof
thus
IT c= NAT *
TREES_1:def 5 ( ( for p being FinSequence of NAT st p in IT holds
ProperPrefixes p c= IT ) & ( for p being FinSequence of NAT
for k, n being Element of NAT st p ^ <*k*> in IT & n <= k holds
p ^ <*n*> in IT ) )
thus
for
p being
FinSequence of
NAT st
p in IT holds
ProperPrefixes p c= IT
for p being FinSequence of NAT
for k, n being Element of NAT st p ^ <*k*> in IT & n <= k holds
p ^ <*n*> in IT
let p be
FinSequence of
NAT ;
for k, n being Element of NAT st p ^ <*k*> in IT & n <= k holds
p ^ <*n*> in ITlet k,
m be
Element of
NAT ;
( p ^ <*k*> in IT & m <= k implies p ^ <*m*> in IT )
assume A15:
p ^ <*k*> in IT
;
( not m <= k or p ^ <*m*> in IT )
A16:
(
p ^ <*k*> in { <*j*> where j is Element of NAT : j < n } or
p ^ <*k*> in {{} } )
by A15, XBOOLE_0:def 3;
consider l being
Element of
NAT such that A17:
p ^ <*k*> = <*l*>
and A18:
l < n
by A16, TARSKI:def 1;
A19:
(len p) + (len <*k*>) =
len <*l*>
by A17, FINSEQ_1:35
.=
1
by FINSEQ_1:56
;
A20:
(len p) + 1
= 0 + 1
by A19, FINSEQ_1:56;
A21:
p = {}
by A20;
A22:
<*k*> = <*l*>
by A17, A21, FINSEQ_1:47;
A23:
<*k*> . 1
= k
by FINSEQ_1:def 8;
A24:
k = l
by A22, A23, FINSEQ_1:def 8;
assume A25:
m <= k
;
p ^ <*m*> in IT
A26:
p ^ <*m*> = <*m*>
by A21, FINSEQ_1:47;
A27:
m < n
by A18, A24, A25, XXREAL_0:2;
A28:
p ^ <*m*> in { <*j*> where j is Element of NAT : j < n }
by A26, A27;
thus
p ^ <*m*> in IT
by A28, XBOOLE_0:def 3;
verum
end;
reconsider IT = IT as Tree by A1;
A29:
IT, Seg (n + 1) are_equipotent
proof
defpred S1[
set ,
set ]
means ( ( $1
= {} & $2
= 1 ) or ex
n being
Element of
NAT st
( $1
= <*n*> & $2
= n + 2 ) );
A30:
for
x,
y,
z being
set st
x in IT &
S1[
x,
y] &
S1[
x,
z] holds
y = z
A36:
for
x being
set st
x in IT holds
ex
y being
set st
S1[
x,
y]
consider f being
Function such that A43:
(
dom f = IT & ( for
x being
set st
x in IT holds
S1[
x,
f . x] ) )
from CLASSES1:sch 1(A36);
take
f
;
WELLORD2:def 4 ( f is one-to-one & proj1 f = IT & proj2 f = Seg (n + 1) )
thus
f is
one-to-one
( proj1 f = IT & proj2 f = Seg (n + 1) )
thus
dom f = IT
by A43;
proj2 f = Seg (n + 1)
thus
rng f c= Seg (n + 1)
XBOOLE_0:def 10 Seg (n + 1) is_a_prefix_of proj2 fproof
let x be
set ;
TARSKI:def 3 ( not x in rng f or x in Seg (n + 1) )
assume A57:
x in rng f
;
x in Seg (n + 1)
consider y being
set such that A58:
y in dom f
and A59:
x = f . y
by A57, FUNCT_1:def 5;
A60:
1
<= 1
+ n
by NAT_1:11;
A61:
1
in Seg (n + 1)
by A60, FINSEQ_1:3;
A62:
now given k being
Element of
NAT such that A63:
y = <*k*>
and A64:
x = k + 2
;
x in Seg (n + 1)A65:
(
y in { <*j*> where j is Element of NAT : j < n } or
y in {{} } )
by A43, A58, XBOOLE_0:def 3;
consider l being
Element of
NAT such that A66:
(
y = <*l*> &
l < n )
by A63, A65, TARSKI:def 1;
A67:
(
<*k*> . 1
= k &
<*l*> . 1
= l )
by FINSEQ_1:def 8;
A68:
k + 1
<= n
by A63, A66, A67, NAT_1:13;
A69:
( 1
+ 0 <= (k + 1) + 1 &
(k + 1) + 1
<= n + 1 )
by A68, XREAL_1:9;
thus
x in Seg (n + 1)
by A64, A69, FINSEQ_1:3;
verum end;
thus
x in Seg (n + 1)
by A43, A58, A59, A61, A62;
verum
end;
let x be
set ;
TARSKI:def 3 ( not x in Seg (n + 1) or x in proj2 f )
assume A70:
x in Seg (n + 1)
;
x in proj2 f
reconsider k =
x as
Element of
NAT by A70;
A71:
1
<= k
by A70, FINSEQ_1:3;
A72:
k <= n + 1
by A70, FINSEQ_1:3;
A73:
{} in {{} }
by TARSKI:def 1;
A74:
{} in IT
by A73, XBOOLE_0:def 3;
A75:
S1[
{} ,
f . {} ]
by A43, A74;
A76:
1
in rng f
by A43, A74, A75, FUNCT_1:def 5;
A77:
now assume A78:
1
< k
;
k in rng fA79:
1
+ 1
<= k
by A78, NAT_1:13;
consider m being
Nat such that A80:
k = 2
+ m
by A79, NAT_1:10;
reconsider m =
m as
Element of
NAT by ORDINAL1:def 13;
A81:
(1 + 1) + m = 1
+ (1 + m)
;
A82:
1
+ m <= n
by A72, A80, A81, XREAL_1:8;
A83:
m < n
by A82, NAT_1:13;
A84:
<*m*> in { <*j*> where j is Element of NAT : j < n }
by A83;
A85:
<*m*> in IT
by A84, XBOOLE_0:def 3;
A86:
S1[
<*m*>,
f . <*m*>]
by A43, A85;
A87:
k = f . <*m*>
by A30, A80, A85, A86;
thus
k in rng f
by A43, A85, A87, FUNCT_1:def 5;
verum end;
thus
x in proj2 f
by A71, A76, A77, XXREAL_0:1;
verum
end;
thus
{ <*k*> where k is Element of NAT : k < n } \/ {{} } is finite Tree
by A29, CARD_1:68; verum