theorem :: TREES_3:23

for f being Function holds
( f is FinTree-yielding iff for x being object st x in dom f holds
f . x is finite Tree )