set IT = { <*k*> where k is Nat : k < n } \/ {{}};
{ <*k*> where k is Nat : k < n } \/ {{}} is Tree-like

proof

thus { <*k*> where k is Nat : k < n } \/ {{}} c= NAT * :: according to TREES_1:def 3 :: thesis: ( ( for p being FinSequence of NAT st p in { <*k*> where k is Nat : k < n } \/ {{}} holds
ProperPrefixes p c= { <*k*> where k is Nat : k < n } \/ {{}} ) & ( for p being FinSequence of NAT
for k, n being Nat st p ^ <*k*> in { <*k*> where k is Nat : k < n } \/ {{}} & n <= k holds
p ^ <*n*> in { <*k*> where k is Nat : k < n } \/ {{}} ) )

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { <*k*> where k is Nat : k < n } \/ {{}} or x in NAT * )
assume x in { <*k*> where k is Nat : k < n } \/ {{}} ; :: thesis: x in NAT *
then A1: ( x in { <*k*> where k is Nat : k < n } or x in {{}} ) by XBOOLE_0:def 3;
A2: {} in NAT * by FINSEQ_1:49;

now :: thesis: ( x in { <*k*> where k is Nat : k < n } implies x in NAT * )

assume x in { <*k*> where k is Nat : k < n } ; :: thesis: x in NAT *
then consider k being Nat such that
A3: ( x = <*k*> & k < n ) ;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
x = <*k*> by A3;
hence x in NAT * by FINSEQ_1:def 11; :: thesis: verum

end;

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

end;

thus for p being FinSequence of NAT st p in { <*k*> where k is Nat : k < n } \/ {{}} holds
ProperPrefixes p c= { <*k*> where k is Nat : k < n } \/ {{}} :: thesis: for p being FinSequence of NAT
for k, n being Nat st p ^ <*k*> in { <*k*> where k is Nat : k < n } \/ {{}} & n <= k holds
p ^ <*n*> in { <*k*> where k is Nat : k < n } \/ {{}}

proof

let p be FinSequence of NAT ; :: thesis: ( p in { <*k*> where k is Nat : k < n } \/ {{}} implies ProperPrefixes p c= { <*k*> where k is Nat : k < n } \/ {{}} )
assume p in { <*k*> where k is Nat : k < n } \/ {{}} ; :: thesis: ProperPrefixes p c= { <*k*> where k is Nat : k < n } \/ {{}}
then A4: ( p in { <*k*> where k is Nat : k < n } or p in {{}} ) by XBOOLE_0:def 3;

now :: thesis: ( p in { <*k*> where k is Nat : k < n } implies ProperPrefixes p c= { <*k*> where k is Nat : k < n } \/ {{}} )

assume p in { <*k*> where k is Nat : k < n } ; :: thesis: ProperPrefixes p c= { <*k*> where k is Nat : k < n } \/ {{}}
then ex k being Nat st
( p = <*k*> & k < n ) ;
then ProperPrefixes p = {{}} by Th15;
hence ProperPrefixes p c= { <*k*> where k is Nat : k < n } \/ {{}} by XBOOLE_1:7; :: thesis: verum

end;

hence ProperPrefixes p c= { <*k*> where k is Nat : k < n } \/ {{}} by A4, Th14, TARSKI:def 1; :: thesis: verum

end;

let p be FinSequence of NAT ; :: thesis: for k, n being Nat st p ^ <*k*> in { <*k*> where k is Nat : k < n } \/ {{}} & n <= k holds
p ^ <*n*> in { <*k*> where k is Nat : k < n } \/ {{}}
let k, m be Nat; :: thesis: ( p ^ <*k*> in { <*k*> where k is Nat : k < n } \/ {{}} & m <= k implies p ^ <*m*> in { <*k*> where k is Nat : k < n } \/ {{}} )
assume p ^ <*k*> in { <*k*> where k is Nat : k < n } \/ {{}} ; :: thesis: ( not m <= k or p ^ <*m*> in { <*k*> where k is Nat : k < n } \/ {{}} )
then ( p ^ <*k*> in { <*j*> where j is Nat : j < n } or p ^ <*k*> in {{}} ) by XBOOLE_0:def 3;
then consider l being Nat such that
A5: p ^ <*k*> = <*l*> and
A6: l < n by TARSKI:def 1;
(len p) + (len <*k*>) = len <*l*> by A5, FINSEQ_1:22
.= 1 by FINSEQ_1:39 ;
then (len p) + 1 = 0 + 1 by FINSEQ_1:39;
then A7: p = {} ;
then A8: <*k*> = <*l*> by A5, FINSEQ_1:34;
<*k*> . 1 = k ;
then A9: k = l by A8, FINSEQ_1:def 8;
assume A10: m <= k ; :: thesis: p ^ <*m*> in { <*k*> where k is Nat : k < n } \/ {{}}
A11: p ^ <*m*> = <*m*> by A7, FINSEQ_1:34;
m < n by A6, A9, A10, XXREAL_0:2;
then p ^ <*m*> in { <*j*> where j is Nat : j < n } by A11;
hence p ^ <*m*> in { <*k*> where k is Nat : k < n } \/ {{}} by XBOOLE_0:def 3; :: thesis: verum

end;

hence { <*k*> where k is Nat : k < n } \/ {{}} is Tree ; :: thesis: verum