let f be Function; :: thesis: ( f is FinTree-yielding implies f is Tree-yielding )
assume f is FinTree-yielding ; :: thesis: f is Tree-yielding
then rng f is constituted-FinTrees set by Def10;
hence rng f is constituted-Trees ; :: according to TREES_3:def 9 :: thesis: verum