theorem Th14: :: TREES_A:14

for T, T1 being DecoratedTree
for P being AntiChain_of_Prefixes of dom T
for q being FinSequence of NAT st q in dom (tree (T,P,T1)) & q in { (p ^ s) where p is Element of dom T, s is Element of dom T1 : p in P } holds
ex p9 being Element of dom T ex r being Element of dom T1 st
( q = p9 ^ r & p9 in P & (tree (T,P,T1)) . q = T1 . r )