theorem :: TREES_4:17

for x, y being object
for p being FinSequence st root-tree x = y -tree p & p is DTree-yielding holds
( x = y & p = {} )