let p be FinSequence of NAT ; :: thesis: for T, T1 being DecoratedTree st p in dom T holds

for q being FinSequence of NAT holds

( not q in dom (T with-replacement (p,T1)) or ( 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 ) )

let T, T1 be DecoratedTree; :: thesis: ( p in dom T implies for q being FinSequence of NAT holds

( not q in dom (T with-replacement (p,T1)) or ( 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 ) ) )

assume A1: p in dom T ; :: thesis: for q being FinSequence of NAT holds

( not q in dom (T with-replacement (p,T1)) or ( 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 ) )

let q be FinSequence of NAT ; :: thesis: ( not q in dom (T with-replacement (p,T1)) or ( 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 ) )

assume q in dom (T with-replacement (p,T1)) ; :: thesis: ( ( 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 ) )

then q in (dom T) with-replacement (p,(dom T1)) by A1, TREES_2:def 11;

hence ( ( 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, TREES_2:def 11; :: thesis: verum

for q being FinSequence of NAT holds

( not q in dom (T with-replacement (p,T1)) or ( 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 ) )

let T, T1 be DecoratedTree; :: thesis: ( p in dom T implies for q being FinSequence of NAT holds

( not q in dom (T with-replacement (p,T1)) or ( 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 ) ) )

assume A1: p in dom T ; :: thesis: for q being FinSequence of NAT holds

( not q in dom (T with-replacement (p,T1)) or ( 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 ) )

let q be FinSequence of NAT ; :: thesis: ( not q in dom (T with-replacement (p,T1)) or ( 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 ) )

assume q in dom (T with-replacement (p,T1)) ; :: thesis: ( ( 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 ) )

then q in (dom T) with-replacement (p,(dom T1)) by A1, TREES_2:def 11;

hence ( ( 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, TREES_2:def 11; :: thesis: verum