theorem Th11: :: TREES_A:11

for p being FinSequence of NAT
for T, T1 being DecoratedTree st p in dom T holds
for q being FinSequence of NAT holds
( not q in dom (T with-replacement (p,T1)) or ( not p is_a_prefix_of q & (T with-replacement (p,T1)) . q = T . q ) or ex r being FinSequence of NAT st
( r in dom T1 & q = p ^ r & (T with-replacement (p,T1)) . q = T1 . r ) )