let T be Tree; :: thesis: ^ T = (elementary_tree 1) with-replacement (<*0*>,T)
let p be FinSequence of NAT ; :: according to TREES_2:def 1 :: thesis: ( ( not p in ^ T or p in (elementary_tree 1) with-replacement (<*0*>,T) ) & ( not p in (elementary_tree 1) with-replacement (<*0*>,T) or p in ^ T ) )
A1: <*T*> . 1 = T ;
A2: len <*T*> = 1 by FINSEQ_1:40;
A3: 0 + 1 = 1 ;
A4: {} in T by TREES_1:22;
A5: <*0*> in elementary_tree 1 by TARSKI:def 2, TREES_1:51;
thus ( p in ^ T implies p in (elementary_tree 1) with-replacement (<*0*>,T) ) :: thesis: ( not p in (elementary_tree 1) with-replacement (<*0*>,T) or p in ^ T )

proof

assume A6: p in ^ T ; :: thesis: p in (elementary_tree 1) with-replacement (<*0*>,T)

now :: thesis: ( p <> {} implies p in (elementary_tree 1) with-replacement (<*0*>,T) )

assume p <> {} ; :: thesis: p in (elementary_tree 1) with-replacement (<*0*>,T)
then consider n being Nat, q being FinSequence such that
A7: n < len <*T*> and
A8: q in <*T*> . (n + 1) and
A9: p = <*n*> ^ q by A6, Def15;
reconsider q = q as FinSequence of NAT by A9, FINSEQ_1:36;
A10: n = 0 by A2, A3, A7, NAT_1:13;
p = <*n*> ^ q by A9;
hence p in (elementary_tree 1) with-replacement (<*0*>,T) by A5, A8, A10, TREES_1:def 9; :: thesis: verum

end;

hence p in (elementary_tree 1) with-replacement (<*0*>,T) by TREES_1:22; :: thesis: verum

end;

assume p in (elementary_tree 1) with-replacement (<*0*>,T) ; :: thesis: p in ^ T
then A11: ( ( p in elementary_tree 1 & not <*0*> is_a_proper_prefix_of p ) or ex r being FinSequence of NAT st
( r in T & p = <*0*> ^ r ) ) by A5, TREES_1:def 9;

now :: thesis: ( p in elementary_tree 1 implies p in ^ T )

assume p in elementary_tree 1 ; :: thesis: p in ^ T
then ( p = {} or ( p = <*0*> & p ^ {} = p ) ) by FINSEQ_1:34, TARSKI:def 2, TREES_1:51;
hence p in ^ T by A1, A2, A3, A4, Def15; :: thesis: verum

end;

hence p in ^ T by A1, A2, A3, A11, Def15; :: thesis: verum