let D1, D2 be DecoratedTree; ( 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 ) )
; D1 = D2
hence
D1 = D2
by A6, A8, Th31; verum