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 12;
then consider x being object such that
A1: succ (Root Z) = {x} by CARD_2:42;
A2: x in succ (Root Z) by A1, TARSKI:def 1;
then reconsider x9 = x as Element of Z ;
x9 in { ((Root Z) ^ <*n*>) where n is Nat : (Root Z) ^ <*n*> in Z } by A2, TREES_2:def 5;
then consider m being Nat such that
A3: x9 = (Root Z) ^ <*m*> and
A4: (Root Z) ^ <*m*> in Z ;
A5: x9 = <*m*> by A3, FINSEQ_1:34;
now :: thesis: not m <> 0
A6: <*0*> = (Root Z) ^ <*0*> by FINSEQ_1:34;
<*m*> in Z by A4, FINSEQ_1:34;
then <*0*> in Z by Th3, NAT_1:2;
then (Root Z) ^ <*0*> in succ (Root Z) by A6, TREES_2:12;
then A7: <*0*> = x by A1, A6, TARSKI:def 1;
assume m <> 0 ; :: thesis: contradiction
hence contradiction by A5, A7, TREES_1:3; :: thesis: verum
end;
hence succ (Root Z) = {<*0*>} by A1, A3, FINSEQ_1:34; :: thesis: verum