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