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