set X = {0,1} * ;
A1: now :: thesis: for p being FinSequence of NAT st p in {0,1} * holds
ProperPrefixes p c= {0,1} *
let p be FinSequence of NAT ; :: thesis: ( p in {0,1} * implies ProperPrefixes p c= {0,1} * )
assume A2: p in {0,1} * ; :: thesis:
thus ProperPrefixes p c= {0,1} * :: thesis: verum
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in ProperPrefixes p or y in {0,1} * )
assume y in ProperPrefixes p ; :: thesis: y in {0,1} *
then consider q being FinSequence such that
A3: y = q and
A4: q is_a_proper_prefix_of p by TREES_1:def 2;
q is_a_prefix_of p by A4;
then ex n being Nat st q = p | (Seg n) by TREES_1:def 1;
hence y in {0,1} * by A2, A3, Th1; :: thesis: verum
end;
end;
A5: now :: thesis: for p being FinSequence of NAT
for k, n being Nat st p ^ <*k*> in {0,1} * & n <= k holds
p ^ <*n*> in {0,1} *
let p be FinSequence of NAT ; :: thesis: for k, n being Nat st p ^ <*k*> in {0,1} * & n <= k holds
p ^ <*n*> in {0,1} *

let k, n be Nat; :: thesis: ( p ^ <*k*> in {0,1} * & n <= k implies p ^ <*n*> in {0,1} * )
assume that
A6: p ^ <*k*> in {0,1} * and
A7: n <= k ; :: thesis: p ^ <*n*> in {0,1} *
A8: p ^ <*k*> is FinSequence of {0,1} by ;
then reconsider kk = <*k*> as FinSequence of {0,1} by FINSEQ_1:36;
1 in Seg 1 by FINSEQ_1:3;
then 1 in dom <*k*> by FINSEQ_1:38;
then kk . 1 in {0,1} by FINSEQ_2:11;
then A9: k in {0,1} by FINSEQ_1:40;
now :: thesis: ( n = 0 or n = 1 )
per cases ( k = 0 or k = 1 ) by ;
suppose k = 0 ; :: thesis: ( n = 0 or n = 1 )
hence ( n = 0 or n = 1 ) by A7; :: thesis: verum
end;
suppose A10: k = 1 ; :: thesis: ( n = 0 or n = 1 )
( n = 1 or n = 0 )
proof
assume n <> 1 ; :: thesis: n = 0
then n < 0 + 1 by ;
hence n = 0 by NAT_1:13; :: thesis: verum
end;
hence ( n = 0 or n = 1 ) ; :: thesis: verum
end;
end;
end;
then n in {0,1} by TARSKI:def 2;
then A11: <*n*> is FinSequence of {0,1} by Lm2;
p is FinSequence of {0,1} by ;
then p ^ <*n*> is FinSequence of {0,1} by ;
hence p ^ <*n*> in {0,1} * by FINSEQ_1:def 11; :: thesis: verum
end;
{0,1} * c= NAT * by FINSEQ_1:62;
hence {0,1} * is Tree by ; :: thesis: verum