ex p being non empty DTree-yielding FinSequence st
( dom p = dom F₁() & p . 1 = F₂() & ( for i, j being Element of dom F₁() st j = i + 1 holds
for d being DecoratedTree st d = p . i holds
p . j = F₃(i,d) ) )