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

now :: thesis:

let q be FinSequence of NAT ; :: thesis:
assume that
A11: q in dom D1 and
A12: D1 . q <> D2 . q ; :: thesis:
thus contradiction :: thesis:

proof

per cases by A7, A8, A11;

suppose A13: for p being FinSequence of NAT st p in P holds
( not p is_a_prefix_of q & D1 . q = T . q ) ; :: thesis:

now :: thesis:

per cases by A7, A10, A11;

suppose A14: for p being FinSequence of NAT st p in P holds
( not p is_a_prefix_of q & D2 . q = T . q ) ; :: thesis:

consider x being object such that
A15: x in P by A1, XBOOLE_0:def 1;
P c= dom T by TREES_1:def 11;
then reconsider x = x as Element of dom T by A15;
A16: ex p9 being FinSequence of NAT st p9 = x ;
then D1 . q = T . q by A13, A15;
hence contradiction by A12, A14, A15, A16; :: thesis:

end;

suppose ex p, r being FinSequence of NAT st
( p in P & r in dom T1 & q = p ^ r & D2 . q = T1 . r ) ; :: thesis:

then consider p2, r2 being FinSequence of NAT such that
A17: p2 in P and
r2 in dom T1 and
A18: q = p2 ^ r2 and
D2 . q = T1 . r2 ;
not p2 is_a_prefix_of q by A13, A17;
hence contradiction by A18, TREES_1:1; :: thesis:

end;

end;

end;

hence contradiction ; :: thesis:

end;

suppose ex p, r being FinSequence of NAT st
( p in P & r in dom T1 & q = p ^ r & D1 . q = T1 . r ) ; :: thesis:

then consider p1, r1 being FinSequence of NAT such that
A19: p1 in P and
r1 in dom T1 and
A20: q = p1 ^ r1 and
A21: D1 . q = T1 . r1 ;

now :: thesis:

per cases by A7, A10, A11;

suppose for p being FinSequence of NAT st p in P holds
( not p is_a_prefix_of q & D2 . q = T . q ) ; :: thesis:

then not p1 is_a_prefix_of q by A19;
hence contradiction by A20, TREES_1:1; :: thesis:

end;

suppose ex p, r being FinSequence of NAT st
( p in P & r in dom T1 & q = p ^ r & D2 . q = T1 . r ) ; :: thesis:

then consider p2, r2 being FinSequence of NAT such that
A22: p2 in P and
r2 in dom T1 and
A23: q = p2 ^ r2 and
A24: D2 . q = T1 . r2 ;

now :: thesis:

assume A25: p1 <> p2 ; :: thesis:
p1,p2 are_c=-comparable by A20, A23, Th1;
hence contradiction by A19, A22, A25, TREES_1:def 10; :: thesis:

end;

hence contradiction by A12, A20, A21, A23, A24, FINSEQ_1:33; :: thesis:

end;

end;

end;

hence contradiction ; :: thesis:

end;

end;

end;

end;

hence D1 = D2 by A7, A9, TREES_2:31; :: thesis: