for T, T1 being DecoratedTree
for P being AntiChain_of_Prefixes of dom T st P <> {} holds
for q being FinSequence of NAT st q in dom (tree (T,P,T1)) & q in { t1 where t1 is Element of dom T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1 } holds
(tree (T,P,T1)) . q = T . q