consider d being Element of D;
reconsider T = {{} } as Tree by TREES_1:48;
take T --> d ; :: thesis: T --> d is finite
dom (T --> d) is finite by FUNCOP_1:19;
hence T --> d is finite by Lm2; :: thesis: verum