consider T being finite Tree;
consider t being Function of T,D;
dom t is finite ;
hence not FinTrees D is empty by Def8; :: thesis: verum