for D1, D2 being non empty set
for d1 being Element of D1
for d2 being Element of D2
for F being non empty DTree-set of D1,D2
for F2 being non empty DTree-set of D2
for p being FinSequence of F
for p2 being FinSequence of F2 st dom p2 = dom p & ( for i being Nat st i in dom p holds
for T being DecoratedTree of D1,D2 st T = p . i holds
p2 . i = T `2 ) holds
([d1,d2] -tree p) `2 = d2 -tree p2