let D1, D2 be DecoratedTree; :: thesis:
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:

let q be FinSequence of NAT ; :: thesis:
assume that
A10: q in dom D1 and
A11: D1 . q <> D2 . q ; :: thesis:
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:

end;