reconsider q = doms p as FinTree-yielding FinSequence ;
dom (x -tree p) = tree q by TREES_4:10;
hence x -tree p is finite by FINSET_1:10; :: thesis: verum