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