let p be FinSequence of NAT ; :: thesis: for T, T1 being DecoratedTree st p in dom T holds
for q being FinSequence of NAT st q in dom (T with-replacement p,T1) & q in { t1 where t1 is Element of dom T : not p is_a_prefix_of t1 } holds
(T with-replacement p,T1) . q = T . q
let T, T1 be DecoratedTree; :: thesis: ( p in dom T implies for q being FinSequence of NAT st q in dom (T with-replacement p,T1) & q in { t1 where t1 is Element of dom T : not p is_a_prefix_of t1 } holds
(T with-replacement p,T1) . q = T . q )
assume A1: p in dom T ; :: thesis: for q being FinSequence of NAT st q in dom (T with-replacement p,T1) & q in { t1 where t1 is Element of dom T : not p is_a_prefix_of t1 } holds
(T with-replacement p,T1) . q = T . q
let q be FinSequence of NAT ; :: thesis: ( q in dom (T with-replacement p,T1) & q in { t1 where t1 is Element of dom T : not p is_a_prefix_of t1 } implies (T with-replacement p,T1) . q = T . q )
assume A2: ( q in dom (T with-replacement p,T1) & q in { t1 where t1 is Element of dom T : not p is_a_prefix_of t1 } ) ; :: thesis: (T with-replacement p,T1) . q = T . q

per cases ( ( not p is_a_prefix_of q & (T with-replacement p,T1) . q = T . q ) or ex r being FinSequence of NAT st
( r in dom T1 & q = p ^ r & (T with-replacement p,T1) . q = T1 . r ) ) by A1, A2, Th14;

suppose ( not p is_a_prefix_of q & (T with-replacement p,T1) . q = T . q ) ; :: thesis: (T with-replacement p,T1) . q = T . q

hence (T with-replacement p,T1) . q = T . q ; :: thesis: verum

end;

suppose ex r being FinSequence of NAT st
( r in dom T1 & q = p ^ r & (T with-replacement p,T1) . q = T1 . r ) ; :: thesis: (T with-replacement p,T1) . q = T . q

then consider r being FinSequence of NAT such that
A3: ( r in dom T1 & q = p ^ r & (T with-replacement p,T1) . q = T1 . r ) ;
consider t' being Element of dom T such that
A4: ( q = t' & not p is_a_prefix_of t' ) by A2;
thus (T with-replacement p,T1) . q = T . q by A3, A4, TREES_1:8; :: thesis: verum

end;

end;