let x be Element of dom (T | t); :: according to TREES_9:def 2,TREES_9:def 4 :: thesis: succ x is finite
A1: dom (T | t) = (dom T) | t by TREES_2:def 10;
then x in (dom T) | t ;
then reconsider tx = t ^ x as Element of dom T by TREES_1:def 6;
dom T = (dom T) with-replacement (t,((dom T) | t)) by TREES_2:6;
then succ tx, succ x are_equipotent by A1, TREES_2:37;
then card (succ x) = card (succ tx) by CARD_1:5;
hence succ x is finite ; :: thesis: verum