let Z be finite Tree; :: thesis:
let z be Element of Z; :: thesis:
set e = elementary_tree 1;
A1: <*0*> in elementary_tree 1 by TARSKI:def 2, TREES_1:51;
A2: {} in Z by TREES_1:22;
assume A3: succ (Root Z) = {z} ; :: thesis:
then card (succ (Root Z)) = 1 by CARD_1:30;
then branchdeg (Root Z) = 1 by TREES_2:def 12;
then {z} = {<*0*>} by A3, Th13;
then z in {<*0*>} by TARSKI:def 1;
then A4: z = <*0*> by TARSKI:def 1;
then A5: <*0*> in Z ;

let x be object ; :: thesis:
thus ( x in Z implies x in (elementary_tree 1) with-replacement (<*0*>,(Z | z)) ) :: thesis:

assume x in Z ; :: thesis:
then reconsider x9 = x as Element of Z ;

suppose x9 = {} ; :: thesis:

hence x in (elementary_tree 1) with-replacement (<*0*>,(Z | z)) by TREES_1:22; :: thesis:

end;

suppose x9 <> {} ; :: thesis:

then consider w being FinSequence of NAT , n being Element of NAT such that
A6: x9 = <*n*> ^ w by FINSEQ_2:130;
<*n*> is_a_prefix_of x9 by A6, TREES_1:1;
then A7: <*n*> in Z by TREES_1:20;
<*n*> = (Root Z) ^ <*n*> by FINSEQ_1:34;
then A8: <*n*> in succ (Root Z) by A7, TREES_2:12;
then <*n*> = z by A3, TARSKI:def 1;
then A9: w in Z | z by A6, TREES_1:def 6;
<*n*> = <*0*> by A3, A4, A8, TARSKI:def 1;
hence x in (elementary_tree 1) with-replacement (<*0*>,(Z | z)) by A1, A6, A9, TREES_1:def 9; :: thesis:

end;

end;

end;

assume x in (elementary_tree 1) with-replacement (<*0*>,(Z | z)) ; :: thesis:
then reconsider x9 = x as Element of (elementary_tree 1) with-replacement (<*0*>,(Z | z)) ;

per cases by A1, TREES_1:def 9;

suppose ( x9 in elementary_tree 1 & not <*0*> is_a_proper_prefix_of x9 ) ; :: thesis:

hence x in Z by A5, A2, TARSKI:def 2, TREES_1:51; :: thesis:

end;

suppose ex s being FinSequence of NAT st
( s in Z | z & x9 = <*0*> ^ s ) ; :: thesis:

hence x in Z by A4, TREES_1:def 6; :: thesis:

end;

end;

end;

hence Z = (elementary_tree 1) with-replacement (<*0*>,(Z | z)) by TARSKI:2; :: thesis: