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 p being FinSequence of F ex p1 being FinSequence of Trees D1 st
( dom p1 = dom p & ( for i being Nat st i in dom p holds
ex T being Element of F st
( T = p . i & p1 . i = T `1 ) ) & ([d1,d2] -tree p) `1 = d1 -tree p1 )