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