theorem Th24: :: TREES_3:24
for f being Function holds
( f is DTree-yielding iff for x being object st x in dom f holds
f . x is DecoratedTree )