let F be Function; :: thesis: ( F is empty implies ( F is Tree-yielding & F is FinTree-yielding & F is DTree-yielding ) )
assume A1: F is empty ; :: thesis: ( F is Tree-yielding & F is FinTree-yielding & F is DTree-yielding )
hence rng F is constituted-Trees ; :: according to TREES_3:def 9 :: thesis: ( F is FinTree-yielding & F is DTree-yielding )
thus rng F is constituted-FinTrees by A1; :: according to TREES_3:def 10 :: thesis: F is DTree-yielding
thus rng F is constituted-DTrees by A1; :: according to TREES_3:def 11 :: thesis: verum