theorem Th22: :: TREES_3:22

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