let Z be finite Tree; :: thesis: for z being Element of Z st succ (Root Z) = {z} holds
Z = (elementary_tree 1) with-replacement (<*0*>,(Z | z))
let z be Element of Z; :: thesis: ( succ (Root Z) = {z} implies Z = (elementary_tree 1) with-replacement (<*0*>,(Z | z)) )
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: Z = (elementary_tree 1) with-replacement (<*0*>,(Z | z))
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 ;

now :: thesis: for x being object holds
( ( x in Z implies x in (elementary_tree 1) with-replacement (<*0*>,(Z | z)) ) & ( x in (elementary_tree 1) with-replacement (<*0*>,(Z | z)) implies x in Z ) )

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

proof

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

per cases ( x9 = {} or x9 <> {} ) ;

suppose x9 = {} ; :: thesis: x in (elementary_tree 1) with-replacement (<*0*>,(Z | z))

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

end;

suppose x9 <> {} ; :: thesis: x in (elementary_tree 1) with-replacement (<*0*>,(Z | z))

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: verum

end;

end;

end;

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

per cases ( ( x9 in elementary_tree 1 & not <*0*> is_a_proper_prefix_of x9 ) or ex s being FinSequence of NAT st
( s in Z | z & x9 = <*0*> ^ s ) ) by A1, TREES_1:def 9;

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

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

end;

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

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

end;

end;

end;

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