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

let q be FinSequence of NAT ; :: thesis: ( q in dom D1 implies not D1 . q <> D2 . q )
assume A10: ( q in dom D1 & D1 . q <> D2 . q ) ; :: thesis: contradiction
then A11: ( ( 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;
( ( 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 A10, A11, FINSEQ_1:46, TREES_1:8; :: thesis: verum

end;

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