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
( p is_a_prefix_of p ^ q & p ^ q in (dom T) with-replacement p,(dom T') & dom (T with-replacement p,T') = (dom T) with-replacement p,(dom T') ) by TREES_1:8, TREES_1:def 12, TREES_2:def 12;
then consider r being FinSequence of NAT such that
A1: ( r in dom T' & p ^ q = p ^ r & (T with-replacement p,T') . (p ^ q) = T' . r ) by TREES_2:def 12;
thus (T with-replacement p,T') . (p ^ q) = T' . q by A1, FINSEQ_1:46; :: thesis: verum