reconsider IT = { <*k*> where k is Element of NAT : k < n } \/ {{} } as non empty set ;
IT is Tree-like

proof

thus IT c= NAT * :: according to TREES_1:def 5 :: thesis: ( ( 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 ) )

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in IT or x in NAT * )
assume x in IT ; :: thesis: x in NAT *
then A1: ( ( x in { <*k*> where k is Element of NAT : k < n } or x in {{} } ) & {} in NAT * ) by FINSEQ_1:66, XBOOLE_0:def 3;

now

assume x in { <*k*> where k is Element of NAT : k < n } ; :: thesis: x in NAT *
then ex k being Element of NAT st
( x = <*k*> & k < n ) ;
hence x in NAT * by FINSEQ_1:def 11; :: thesis: verum

end;

hence x in NAT * by A1, TARSKI:def 1; :: thesis: verum

end;

thus for p being FinSequence of NAT st p in IT holds
ProperPrefixes p c= IT :: thesis: 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

proof

let p be FinSequence of NAT ; :: thesis: ( p in IT implies ProperPrefixes p c= IT )
assume p in IT ; :: thesis: ProperPrefixes p c= IT
then A2: ( ( p in { <*k*> where k is Element of NAT : k < n } or p in {{} } ) & {} in NAT * & {} c= IT & ProperPrefixes {} = {} ) by Th39, FINSEQ_1:66, XBOOLE_0:def 3, XBOOLE_1:2;

now

assume p in { <*k*> where k is Element of NAT : k < n } ; :: thesis: ProperPrefixes p c= IT
then ex k being Element of NAT st
( p = <*k*> & k < n ) ;
then ProperPrefixes p = {{} } by Th40;
hence ProperPrefixes p c= IT by XBOOLE_1:7; :: thesis: verum

end;

hence ProperPrefixes p c= IT by A2, TARSKI:def 1; :: thesis: verum

end;

let p be FinSequence of NAT ; :: thesis: for k, n being Element of NAT st p ^ <*k*> in IT & n <= k holds
p ^ <*n*> in IT
let k, m be Element of NAT ; :: thesis: ( p ^ <*k*> in IT & m <= k implies p ^ <*m*> in IT )
assume p ^ <*k*> in IT ; :: thesis: ( not m <= k or p ^ <*m*> in IT )
then ( p ^ <*k*> in { <*j*> where j is Element of NAT : j < n } or p ^ <*k*> in {{} } ) by XBOOLE_0:def 3;
then consider l being Element of NAT such that
A3: ( p ^ <*k*> = <*l*> & l < n ) by TARSKI:def 1;
(len p) + (len <*k*>) = len <*l*> by A3, FINSEQ_1:35
.= 1 by FINSEQ_1:56 ;
then (len p) + 1 = 0 + 1 by FINSEQ_1:56;
then A4: p = {} ;
then ( <*k*> = <*l*> & <*k*> . 1 = k ) by A3, FINSEQ_1:47, FINSEQ_1:def 8;
then A5: k = l by FINSEQ_1:def 8;
assume m <= k ; :: thesis: p ^ <*m*> in IT
then ( p ^ <*m*> = <*m*> & m < n ) by A3, A4, A5, FINSEQ_1:47, XXREAL_0:2;
then p ^ <*m*> in { <*j*> where j is Element of NAT : j < n } ;
hence p ^ <*m*> in IT by XBOOLE_0:def 3; :: thesis: verum

end;

then reconsider IT = IT as Tree ;
IT, Seg (n + 1) are_equipotent

proof

defpred S₁[ set , set ] means ( ( $1 = {} & $2 = 1 ) or ex n being Element of NAT st
( $1 = <*n*> & $2 = n + 2 ) );
A6: for x, y, z being set st x in IT & S₁[x,y] & S₁[x,z] holds
y = z

proof

let x, y, z be set ; :: thesis: ( x in IT & S₁[x,y] & S₁[x,z] implies y = z )
assume that
x in IT and
A7: ( ( x = {} & y = 1 ) or ex n being Element of NAT st
( x = <*n*> & y = n + 2 ) ) and
A8: ( ( x = {} & z = 1 ) or ex n being Element of NAT st
( x = <*n*> & z = n + 2 ) ) ; :: thesis: y = z

now

given n1 being Element of NAT such that A9: ( x = <*n1*> & y = n1 + 2 ) ; :: thesis: ( ex n2 being Element of NAT st
( x = <*n2*> & z = n2 + 2 ) implies y = z )
given n2 being Element of NAT such that A10: ( x = <*n2*> & z = n2 + 2 ) ; :: thesis: y = z
( <*n1*> . 1 = n1 & <*n2*> . 1 = n2 ) by FINSEQ_1:def 8;
hence y = z by A9, A10; :: thesis: verum

end;

hence y = z by A7, A8; :: thesis: verum

end;

A11: for x being set st x in IT holds
ex y being set st S₁[x,y]

proof

let x be set ; :: thesis: ( x in IT implies ex y being set st S₁[x,y] )
assume A12: x in IT ; :: thesis: ex y being set st S₁[x,y]

A13: now

assume x in { <*k*> where k is Element of NAT : k < n } ; :: thesis: ex y being set st S₁[x,y]
then consider k being Element of NAT such that
A14: ( x = <*k*> & k < n ) ;
reconsider y = k + 2 as set ;
take y = y; :: thesis: S₁[x,y]
thus S₁[x,y] by A14; :: thesis: verum

end;

now

assume A15: x in {{} } ; :: thesis: ex y being set st S₁[x,y]
reconsider y = 1 as set ;
take y = y; :: thesis: S₁[x,y]
thus S₁[x,y] by A15, TARSKI:def 1; :: thesis: verum

end;

hence ex y being set st S₁[x,y] by A12, A13, XBOOLE_0:def 3; :: thesis: verum

end;

consider f being Function such that
A16: ( dom f = IT & ( for x being set st x in IT holds
S₁[x,f . x] ) ) from CLASSES1:sch 1(A11);
take f ; :: according to WELLORD2:def 4 :: thesis: ( f is one-to-one & dom f = IT & rng f = Seg (n + 1) )
thus f is one-to-one :: thesis: ( dom f = IT & rng f = Seg (n + 1) )

proof

let x be set ; :: according to FUNCT_1:def 8 :: thesis: for b₁ being set holds
( not x in dom f or not b₁ in dom f or not f . x = f . b₁ or x = b₁ )
let y be set ; :: thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y )
assume A17: ( x in dom f & y in dom f & f . x = f . y ) ; :: thesis: x = y
then A18: ( ( ( x = {} & f . x = 1 ) or ex n being Element of NAT st
( x = <*n*> & f . x = n + 2 ) ) & ( ( y = {} & f . y = 1 ) or ex n being Element of NAT st
( y = <*n*> & f . y = n + 2 ) ) ) by A16;

A19: now

assume A20: ( x = {} & f . x = 1 ) ; :: thesis: for n being Element of NAT holds
( not y = <*n*> or not f . y = n + 2 )
given n being Element of NAT such that A21: ( y = <*n*> & f . y = n + 2 ) ; :: thesis: contradiction
0 + 1 = (n + 1) + 1 by A17, A20, A21;
hence contradiction ; :: thesis: verum

end;

now

assume A22: ( y = {} & f . y = 1 ) ; :: thesis: for n being Element of NAT holds
( not x = <*n*> or not f . x = n + 2 )
given n being Element of NAT such that A23: ( x = <*n*> & f . x = n + 2 ) ; :: thesis: contradiction
0 + 1 = (n + 1) + 1 by A17, A22, A23;
hence contradiction ; :: thesis: verum

end;

hence x = y by A17, A18, A19; :: thesis: verum

end;

thus dom f = IT by A16; :: thesis: rng f = Seg (n + 1)
thus rng f c= Seg (n + 1) :: according to XBOOLE_0:def 10 :: thesis: Seg (n + 1) is_a_prefix_of rng f

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in Seg (n + 1) )
assume x in rng f ; :: thesis: x in Seg (n + 1)
then consider y being set such that
A24: ( y in dom f & x = f . y ) by FUNCT_1:def 5;
( 1 <= 1 & 1 <= 1 + n & 1 + n = n + 1 ) by NAT_1:11;
then A25: 1 in Seg (n + 1) by FINSEQ_1:3;

now

given k being Element of NAT such that A26: ( y = <*k*> & x = k + 2 ) ; :: thesis: x in Seg (n + 1)
( y in { <*j*> where j is Element of NAT : j < n } or y in {{} } ) by A16, A24, XBOOLE_0:def 3;
then consider l being Element of NAT such that
A27: ( y = <*l*> & l < n ) by A26, TARSKI:def 1;
( <*k*> . 1 = k & <*l*> . 1 = l ) by FINSEQ_1:def 8;
then ( k + 1 <= n & 0 <= k + 1 ) by A26, A27, NAT_1:13;
then ( 1 + 0 <= (k + 1) + 1 & (k + 1) + 1 <= n + 1 & (k + 1) + 1 = k + (1 + 1) ) by XREAL_1:9;
hence x in Seg (n + 1) by A26, FINSEQ_1:3; :: thesis: verum

end;

hence x in Seg (n + 1) by A16, A24, A25; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Seg (n + 1) or x in rng f )
assume A28: x in Seg (n + 1) ; :: thesis: x in rng f
then reconsider k = x as Element of NAT ;
A29: ( 1 <= k & k <= n + 1 ) by A28, FINSEQ_1:3;
{} in {{} } by TARSKI:def 1;
then A30: {} in IT by XBOOLE_0:def 3;
then ( S₁[ {} ,1] & S₁[ {} ,f . {} ] ) by A16;
then A31: 1 in rng f by A16, A30, FUNCT_1:def 5;

now

assume 1 < k ; :: thesis: k in rng f
then 1 + 1 <= k by NAT_1:13;
then consider m being Nat such that
A32: k = 2 + m by NAT_1:10;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
(1 + 1) + m = 1 + (1 + m) ;
then ( 1 + m <= n & m + 1 = 1 + m ) by A29, A32, XREAL_1:8;
then m < n by NAT_1:13;
then ( <*m*> in { <*j*> where j is Element of NAT : j < n } & m + 2 = 2 + m ) ;
then A33: ( <*m*> in IT & ex n being Element of NAT st
( <*m*> = <*n*> & k = n + 2 ) ) by A32, XBOOLE_0:def 3;
then ( S₁[<*m*>,k] & S₁[<*m*>,f . <*m*>] ) by A16;
then k = f . <*m*> by A6, A33;
hence k in rng f by A16, A33, FUNCT_1:def 5; :: thesis: verum

end;

hence x in rng f by A29, A31, XXREAL_0:1; :: thesis: verum

end;

hence { <*k*> where k is Element of NAT : k < n } \/ {{} } is finite Tree by CARD_1:68; :: thesis: verum