theorem Th11: :: TREES_4:11

for x, y being object
for p being DTree-yielding FinSequence holds
( y in dom (x -tree p) iff ( y = {} or ex i being Nat ex T being DecoratedTree ex q being Node of T st
( i < len p & T = p . (i + 1) & y = <*i*> ^ q ) ) )