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