for x being object
for p being DTree-yielding FinSequence holds dom (x -tree p) = tree (doms p)