let T, T9 be DecoratedTree; :: thesis: for p being Element of dom T
for q being Element of dom T9 holds (T with-replacement (p,T9)) . (p ^ q) = T9 . q
let p be Element of dom T; :: thesis: for q being Element of dom T9 holds (T with-replacement (p,T9)) . (p ^ q) = T9 . q
let q be Element of dom T9; :: thesis: (T with-replacement (p,T9)) . (p ^ q) = T9 . q
A1: p is_a_prefix_of p ^ q by TREES_1:1;
p ^ q in (dom T) with-replacement (p,(dom T9)) by TREES_1:def 9;
then ex r being FinSequence of NAT st
( r in dom T9 & p ^ q = p ^ r & (T with-replacement (p,T9)) . (p ^ q) = T9 . r ) by A1, TREES_2:def 11;
hence (T with-replacement (p,T9)) . (p ^ q) = T9 . q by FINSEQ_1:33; :: thesis: verum