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