theorem Th31: :: TREES_1:32

for p being FinSequence of NAT
for T, T1 being Tree st p in T holds
T with-replacement (p,T1) = { t1 where t1 is Element of T : not p is_a_proper_prefix_of t1 } \/ { (p ^ s) where s is Element of T1 : verum }