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