let Z be finite Tree; :: thesis: ( branchdeg (Root Z) = 1 implies succ (Root Z) = {<*0 *>} )
assume branchdeg (Root Z) = 1 ; :: thesis: succ (Root Z) = {<*0 *>}
then card (succ (Root Z)) = 1 by TREES_2:def 13;
then consider x being set such that
A1: succ (Root Z) = {x} by CARD_2:60;
A2: x in succ (Root Z) by A1, TARSKI:def 1;
then reconsider x' = x as Element of Z ;
x' in { ((Root Z) ^ <*n*>) where n is Element of NAT : (Root Z) ^ <*n*> in Z } by A2, TREES_2:def 5;
then consider m being Element of NAT such that
A3: ( x' = (Root Z) ^ <*m*> & (Root Z) ^ <*m*> in Z ) ;
A4: x' = <*m*> by A3, FINSEQ_1:47;

now

assume A5: m <> 0 ; :: thesis: contradiction
( <*m*> in Z & 0 <= m ) by A3, FINSEQ_1:47, NAT_1:2;
then A6: <*0 *> in Z by Th11;
A7: <*0 *> = (Root Z) ^ <*0 *> by FINSEQ_1:47;
then (Root Z) ^ <*0 *> in succ (Root Z) by A6, TREES_2:14;
then <*0 *> = x by A1, A7, TARSKI:def 1;
hence contradiction by A4, A5, TREES_1:16; :: thesis: verum

end;

hence succ (Root Z) = {<*0 *>} by A1, A3, FINSEQ_1:47; :: thesis: verum