dom ((elementary_tree 0) --> d) = elementary_tree 0 by FUNCOP_1:19;
hence root-tree d is Element of FinTrees D by TREES_3:def 8; :: thesis: verum