let D1, D2 be DecoratedTree; ( dom D1 = tree ((dom T),P,(dom T1)) & ( for q being FinSequence of NAT holds
( not q in tree ((dom T),P,(dom T1)) or for p being FinSequence of NAT st p in P holds
( not p is_a_prefix_of q & D1 . q = T . q ) or ex p, r being FinSequence of NAT st
( p in P & r in dom T1 & q = p ^ r & D1 . q = T1 . r ) ) ) & dom D2 = tree ((dom T),P,(dom T1)) & ( for q being FinSequence of NAT holds
( not q in tree ((dom T),P,(dom T1)) or for p being FinSequence of NAT st p in P holds
( not p is_a_prefix_of q & D2 . q = T . q ) or ex p, r being FinSequence of NAT st
( p in P & r in dom T1 & q = p ^ r & D2 . q = T1 . r ) ) ) implies D1 = D2 )
assume that
A7:
dom D1 = tree ((dom T),P,(dom T1))
and
A8:
for q being FinSequence of NAT holds
( not q in tree ((dom T),P,(dom T1)) or for p being FinSequence of NAT st p in P holds
( not p is_a_prefix_of q & D1 . q = T . q ) or ex p, r being FinSequence of NAT st
( p in P & r in dom T1 & q = p ^ r & D1 . q = T1 . r ) )
and
A9:
dom D2 = tree ((dom T),P,(dom T1))
and
A10:
for q being FinSequence of NAT holds
( not q in tree ((dom T),P,(dom T1)) or for p being FinSequence of NAT st p in P holds
( not p is_a_prefix_of q & D2 . q = T . q ) or ex p, r being FinSequence of NAT st
( p in P & r in dom T1 & q = p ^ r & D2 . q = T1 . r ) )
; D1 = D2
hence
D1 = D2
by A7, A9, TREES_2:31; verum