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 { (p ^ s) where s is Element of dom T1 : s = s } holds
ex r being Element of dom T1 st
( q = p ^ r & (T with-replacement p,T1) . q = T1 . r )
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 { (p ^ s) where s is Element of dom T1 : s = s } holds
ex r being Element of dom T1 st
( q = p ^ r & (T with-replacement p,T1) . q = T1 . r ) )
assume A1: p in dom T ; :: thesis: for q being FinSequence of NAT st q in dom (T with-replacement p,T1) & q in { (p ^ s) where s is Element of dom T1 : s = s } holds
ex r being Element of dom T1 st
( q = p ^ r & (T with-replacement p,T1) . q = T1 . r )
let q be FinSequence of NAT ; :: thesis: ( q in dom (T with-replacement p,T1) & q in { (p ^ s) where s is Element of dom T1 : s = s } implies ex r being Element of dom T1 st
( q = p ^ r & (T with-replacement p,T1) . q = T1 . r ) )
assume that
A2: q in dom (T with-replacement p,T1) and
A3: q in { (p ^ s) where s is Element of dom T1 : s = s } ; :: thesis: ex r being Element of dom T1 st
( q = p ^ r & (T with-replacement p,T1) . q = T1 . r )

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 A4: ( not p is_a_prefix_of q & (T with-replacement p,T1) . q = T . q ) ; :: thesis: ex r being Element of dom T1 st
( q = p ^ r & (T with-replacement p,T1) . q = T1 . r )

A5: ex r being Element of dom T1 st
( q = p ^ r & r = r ) by A3;
thus ex r being Element of dom T1 st
( q = p ^ r & (T with-replacement p,T1) . q = T1 . r ) by A4, A5, TREES_1:8; :: thesis: verum

end;

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

thus ex r being Element of dom T1 st
( q = p ^ r & (T with-replacement p,T1) . q = T1 . r ) by A6; :: thesis: verum

end;

end;