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