A1: dom (d -tree p) = tree (doms p) by Th10;
thus d -tree p is Element of FinTrees D by A1, TREES_3:def 8; :: thesis: verum