dom (T | t) = (dom T) | t by TREES_2:def 11;
hence T | t is finite by FINSET_1:29; :: thesis: verum