let D1, D2 be DecoratedTree; :: thesis: ( dom D1 = (dom T) with-replacement (p,(dom T1)) & ( for q being FinSequence of NAT holds
( not q in (dom T) with-replacement (p,(dom T1)) or ( not p is_a_prefix_of q & D1 . q = T . q ) or ex r being FinSequence of NAT st
( r in dom T1 & q = p ^ r & D1 . q = T1 . r ) ) ) & dom D2 = (dom T) with-replacement (p,(dom T1)) & ( for q being FinSequence of NAT holds
( not q in (dom T) with-replacement (p,(dom T1)) or ( not p is_a_prefix_of q & D2 . q = T . q ) or ex r being FinSequence of NAT st
( r in dom T1 & q = p ^ r & D2 . q = T1 . r ) ) ) implies D1 = D2 )
assume that
A6: dom D1 = (dom T) with-replacement (p,(dom T1)) and
A7: for q being FinSequence of NAT holds
( not q in (dom T) with-replacement (p,(dom T1)) or ( not p is_a_prefix_of q & D1 . q = T . q ) or ex r being FinSequence of NAT st
( r in dom T1 & q = p ^ r & D1 . q = T1 . r ) ) and
A8: dom D2 = (dom T) with-replacement (p,(dom T1)) and
A9: for q being FinSequence of NAT holds
( not q in (dom T) with-replacement (p,(dom T1)) or ( not p is_a_prefix_of q & D2 . q = T . q ) or ex r being FinSequence of NAT st
( r in dom T1 & q = p ^ r & D2 . q = T1 . r ) ) ; :: thesis: D1 = D2

now :: thesis: for q being FinSequence of NAT st q in dom D1 holds
not D1 . q <> D2 . q

let q be FinSequence of NAT ; :: thesis: ( q in dom D1 implies not D1 . q <> D2 . q )
assume that
A10: q in dom D1 and
A11: D1 . q <> D2 . q ; :: thesis: contradiction
A12: ( ( not p is_a_prefix_of q & D1 . q = T . q ) or ex r being FinSequence of NAT st
( r in dom T1 & q = p ^ r & D1 . q = T1 . r ) ) by A6, A7, A10;
( ( not p is_a_prefix_of q & D2 . q = T . q ) or ex r being FinSequence of NAT st
( r in dom T1 & q = p ^ r & D2 . q = T1 . r ) ) by A6, A9, A10;
hence contradiction by A11, A12, FINSEQ_1:33, TREES_1:1; :: thesis: verum

end;

hence D1 = D2 by A6, A8, Th31; :: thesis: verum