dom (T with-replacement t,T1) = (dom T) with-replacement t,(dom T1) by TREES_2:def 12;
hence T with-replacement t,T1 is finite by FINSET_1:29; :: thesis: verum