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
A10: dom D1 = (dom T) with-replacement p,(dom T1) and
A11: 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
A12: dom D2 = (dom T) with-replacement p,(dom T1) and
A13: 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 that
A15: q in dom D1 and
A16: D1 . q <> D2 . q ; :: thesis: contradiction
A17: ( ( 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 A10, A11, A15;
( ( 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 A10, A13, A15;
hence contradiction by A16, A17, FINSEQ_1:46, TREES_1:8; :: thesis: verum

end;

hence D1 = D2 by A10, A12, Th33; :: thesis: verum