let x be set ; :: thesis: ( <*x*> is FinTree-yielding iff x is finite Tree )
( ( x is finite Tree implies {x} is constituted-FinTrees ) & ( {x} is constituted-FinTrees implies x is finite Tree ) & rng <*x*> = {x} ) by Th14, FINSEQ_1:56;
hence ( <*x*> is FinTree-yielding iff x is finite Tree ) by Def10; :: thesis: verum