reconsider p9 = p as Element of T by A1;
not p is_a_proper_prefix_of p9 ;
then p in { t where t is Element of T : not p is_a_proper_prefix_of t } ;
then reconsider X = { t where t is Element of T : not p is_a_proper_prefix_of t } \/ { (p ^ s) where s is Element of T1 : s = s } as non empty set ;
A4: for x being set st x in { t where t is Element of T : not p is_a_proper_prefix_of t } holds
( x is FinSequence of NAT & x in NAT * & x in T )

proof

let x be set ; :: thesis: ( x in { t where t is Element of T : not p is_a_proper_prefix_of t } implies ( x is FinSequence of NAT & x in NAT * & x in T ) )
assume x in { t where t is Element of T : not p is_a_proper_prefix_of t } ; :: thesis: ( x is FinSequence of NAT & x in NAT * & x in T )
then A6: ex t being Element of T st
( x = t & not p is_a_proper_prefix_of t ) ;
hence x is FinSequence of NAT ; :: thesis: ( x in NAT * & x in T )
thus ( x in NAT * & x in T ) by A6, FINSEQ_1:def 11; :: thesis: verum

end;

X is Tree-like

proof

thus X c= NAT * :: according to TREES_1:def 5 :: thesis: ( ( for p being FinSequence of NAT st p in X holds
ProperPrefixes p c= X ) & ( for p being FinSequence of NAT
for k, n being Element of NAT st p ^ <*k*> in X & n <= k holds
p ^ <*n*> in X ) )

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in NAT * )
assume x in X ; :: thesis: x in NAT *
then A9: ( x in { t where t is Element of T : not p is_a_proper_prefix_of t } or x in { (p ^ s) where s is Element of T1 : s = s } ) by XBOOLE_0:def 3;

now

assume x in { (p ^ s) where s is Element of T1 : s = s } ; :: thesis: x is FinSequence of NAT
then ex s being Element of T1 st
( x = p ^ s & s = s ) ;
hence x is FinSequence of NAT ; :: thesis: verum

end;

hence x in NAT * by A4, A9, FINSEQ_1:def 11; :: thesis: verum

end;

thus for q being FinSequence of NAT st q in X holds
ProperPrefixes q c= X :: thesis: for p being FinSequence of NAT
for k, n being Element of NAT st p ^ <*k*> in X & n <= k holds
p ^ <*n*> in X

proof

let q be FinSequence of NAT ; :: thesis: ( q in X implies ProperPrefixes q c= X )
assume A13: q in X ; :: thesis: ProperPrefixes q c= X

A14: now

assume q in { t where t is Element of T : not p is_a_proper_prefix_of t } ; :: thesis: ProperPrefixes q c= X
then A16: ex t being Element of T st
( q = t & not p is_a_proper_prefix_of t ) ;
then A17: ProperPrefixes q c= T by Def5;
thus ProperPrefixes q c= X :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in ProperPrefixes q or x in X )
assume A18: x in ProperPrefixes q ; :: thesis: x in X
then consider p1 being FinSequence such that
A19: x = p1 and
A20: p1 is_a_proper_prefix_of q by Def4;
reconsider p1 = p1 as Element of T by A17, A18, A19;
not p is_a_proper_prefix_of p1 by A16, A20, XBOOLE_1:56;
then x in { s1 where s1 is Element of T : not p is_a_proper_prefix_of s1 } by A19;
hence x in X by XBOOLE_0:def 3; :: thesis: verum

end;

end;

now

assume q in { (p ^ s) where s is Element of T1 : s = s } ; :: thesis: ProperPrefixes q c= X
then consider s being Element of T1 such that
A25: q = p ^ s and
s = s ;
thus ProperPrefixes q c= X :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in ProperPrefixes q or x in X )
assume A26: x in ProperPrefixes q ; :: thesis: x in X
then reconsider r = x as FinSequence by Th35;
r is_a_proper_prefix_of p ^ s by A25, A26, Th36;
then r is_a_prefix_of p ^ s by XBOOLE_0:def 8;
then consider r1 being FinSequence such that
A29: p ^ s = r ^ r1 by Th8;

A30: now

assume len p <= len r ; :: thesis: r in X
then consider r2 being FinSequence such that
A32: p ^ r2 = r by A29, FINSEQ_1:64;
p ^ s = p ^ (r2 ^ r1) by A29, A32, FINSEQ_1:45;
then s = r2 ^ r1 by FINSEQ_1:46;
then A35: ( dom r2 = Seg (len r2) & s | (dom r2) = r2 ) by FINSEQ_1:33, FINSEQ_1:def 3;
then reconsider r2 = r2 as FinSequence of NAT by FINSEQ_1:23;
r2 is_a_prefix_of s by A35, Def1;
then reconsider r2 = r2 as Element of T1 by Th45;
r = p ^ r2 by A32;
then r in { (p ^ v) where v is Element of T1 : v = v } ;
hence r in X by XBOOLE_0:def 3; :: thesis: verum

end;

now

assume len r <= len p ; :: thesis: r in X
then ex r2 being FinSequence st r ^ r2 = p by A29, FINSEQ_1:64;
then A42: p | (dom r) = r by FINSEQ_1:33;
A43: dom r = Seg (len r) by FINSEQ_1:def 3;
then reconsider r3 = r as FinSequence of NAT by A42, FINSEQ_1:23;
A44: r3 is_a_prefix_of p by A42, A43, Def1;
then A45: not p is_a_proper_prefix_of r3 by XBOOLE_0:def 8;
reconsider r3 = r3 as Element of T by A1, A44, Th45;
r3 in { t where t is Element of T : not p is_a_proper_prefix_of t } by A45;
hence r in X by XBOOLE_0:def 3; :: thesis: verum

end;

hence x in X by A30; :: thesis: verum

end;

end;

hence ProperPrefixes q c= X by A13, A14, XBOOLE_0:def 3; :: thesis: verum

end;

let q be FinSequence of NAT ; :: thesis: for k, n being Element of NAT st q ^ <*k*> in X & n <= k holds
q ^ <*n*> in X
let k, n be Element of NAT ; :: thesis: ( q ^ <*k*> in X & n <= k implies q ^ <*n*> in X )
assume that
A47: q ^ <*k*> in X and
A48: n <= k ; :: thesis: q ^ <*n*> in X

A49: now

assume q ^ <*k*> in { t where t is Element of T : not p is_a_proper_prefix_of t } ; :: thesis: q ^ <*n*> in X
then A51: ex s being Element of T st
( q ^ <*k*> = s & not p is_a_proper_prefix_of s ) ;
then reconsider u = q ^ <*n*> as Element of T by A48, Def5;

now

assume p is_a_proper_prefix_of u ; :: thesis: contradiction
then p is_a_prefix_of q by Th32;
hence contradiction by A51, Th31; :: thesis: verum

end;

then q ^ <*n*> in { t where t is Element of T : not p is_a_proper_prefix_of t } ;
hence q ^ <*n*> in X by XBOOLE_0:def 3; :: thesis: verum

end;

now

assume q ^ <*k*> in { (p ^ s) where s is Element of T1 : s = s } ; :: thesis: q ^ <*n*> in X
then consider s being Element of T1 such that
A58: q ^ <*k*> = p ^ s and
s = s ;

A59: now

assume len q <= len p ; :: thesis: q ^ <*n*> in X
then consider r being FinSequence such that
A61: q ^ r = p by A58, FINSEQ_1:64;
q ^ <*k*> = q ^ (r ^ s) by A58, A61, FINSEQ_1:45;
then A63: <*k*> = r ^ s by FINSEQ_1:46;

A64: now

assume A65: r = <*k*> ; :: thesis: q ^ <*n*> in { t where t is Element of T : not p is_a_proper_prefix_of t }
then reconsider s = q ^ <*n*> as Element of T by A1, A48, A61, Def5;

now

assume A67: p is_a_proper_prefix_of s ; :: thesis: contradiction
then A68: p is_a_prefix_of s by XBOOLE_0:def 8;
len p = (len q) + (len <*k*>) by A61, A65, FINSEQ_1:35
.= (len q) + 1 by FINSEQ_1:57
.= (len q) + (len <*n*>) by FINSEQ_1:57
.= len s by FINSEQ_1:35 ;
hence contradiction by A67, A68, Th15; :: thesis: verum

end;

hence q ^ <*n*> in { t where t is Element of T : not p is_a_proper_prefix_of t } ; :: thesis: verum

end;

now

assume that
A71: s = <*k*> and
A72: r = {} ; :: thesis: q ^ <*n*> in { (p ^ v) where v is Element of T1 : v = v }
( s = {} ^ s & {} = <*> NAT ) by FINSEQ_1:47;
then {} ^ <*n*> in T1 by A48, A71, Def5;
then reconsider t = <*n*> as Element of T1 by FINSEQ_1:47;
q ^ <*n*> = p ^ t by A61, A72, FINSEQ_1:47;
hence q ^ <*n*> in { (p ^ v) where v is Element of T1 : v = v } ; :: thesis: verum

end;

hence q ^ <*n*> in X by A63, A64, FINSEQ_1:109, XBOOLE_0:def 3; :: thesis: verum

end;

now

assume len p <= len q ; :: thesis: q ^ <*n*> in X
then consider r being FinSequence such that
A78: p ^ r = q by A58, FINSEQ_1:64;
p ^ (r ^ <*k*>) = p ^ s by A58, A78, FINSEQ_1:45;
then A80: r ^ <*k*> = s by FINSEQ_1:46;
then ( dom r = Seg (len r) & s | (dom r) = r ) by FINSEQ_1:33, FINSEQ_1:def 3;
then reconsider r = r as FinSequence of NAT by FINSEQ_1:23;
reconsider t = r ^ <*n*> as Element of T1 by A48, A80, Def5;
q ^ <*n*> = p ^ t by A78, FINSEQ_1:45;
then q ^ <*n*> in { (p ^ v) where v is Element of T1 : v = v } ;
hence q ^ <*n*> in X by XBOOLE_0:def 3; :: thesis: verum

end;

hence q ^ <*n*> in X by A59; :: thesis: verum

end;

hence q ^ <*n*> in X by A47, A49, XBOOLE_0:def 3; :: thesis: verum

end;

then reconsider X = X as Tree ;
take X ; :: thesis: for q being FinSequence of NAT holds
( q in X iff ( ( q in T & not p is_a_proper_prefix_of q ) or ex r being FinSequence of NAT st
( r in T1 & q = p ^ r ) ) )
let q be FinSequence of NAT ; :: thesis: ( q in X iff ( ( q in T & not p is_a_proper_prefix_of q ) or ex r being FinSequence of NAT st
( r in T1 & q = p ^ r ) ) )
thus ( not q in X or ( q in T & not p is_a_proper_prefix_of q ) or ex r being FinSequence of NAT st
( r in T1 & q = p ^ r ) ) :: thesis: ( ( ( q in T & not p is_a_proper_prefix_of q ) or ex r being FinSequence of NAT st
( r in T1 & q = p ^ r ) ) implies q in X )

proof

assume A84: q in X ; :: thesis: ( ( q in T & not p is_a_proper_prefix_of q ) or ex r being FinSequence of NAT st
( r in T1 & q = p ^ r ) )

A85: now

assume q in { t where t is Element of T : not p is_a_proper_prefix_of t } ; :: thesis: ( ( q in T & not p is_a_proper_prefix_of q ) or ex r being FinSequence of NAT st
( r in T1 & q = p ^ r ) )
then ex s being Element of T st
( q = s & not p is_a_proper_prefix_of s ) ;
hence ( ( q in T & not p is_a_proper_prefix_of q ) or ex r being FinSequence of NAT st
( r in T1 & q = p ^ r ) ) ; :: thesis: verum

end;

now

assume q in { (p ^ s) where s is Element of T1 : s = s } ; :: thesis: ex r being FinSequence of NAT st
( r in T1 & q = p ^ r )
then ex s being Element of T1 st
( q = p ^ s & s = s ) ;
hence ex r being FinSequence of NAT st
( r in T1 & q = p ^ r ) ; :: thesis: verum

end;

hence ( ( q in T & not p is_a_proper_prefix_of q ) or ex r being FinSequence of NAT st
( r in T1 & q = p ^ r ) ) by A84, A85, XBOOLE_0:def 3; :: thesis: verum

end;

assume A91: ( ( q in T & not p is_a_proper_prefix_of q ) or ex r being FinSequence of NAT st
( r in T1 & q = p ^ r ) ) ; :: thesis: q in X
A92: ( q in T & not p is_a_proper_prefix_of q implies q in { t where t is Element of T : not p is_a_proper_prefix_of t } ) ;
( ex r being FinSequence of NAT st
( r in T1 & q = p ^ r ) implies q in { (p ^ v) where v is Element of T1 : v = v } ) ;
hence q in X by A91, A92, XBOOLE_0:def 3; :: thesis: verum