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

now

let q be FinSequence of NAT ; :: thesis: ( q in dom D1 implies not D1 . q <> D2 . q )
assume A11: ( q in dom D1 & D1 . q <> D2 . q ) ; :: thesis: contradiction
thus contradiction :: thesis: verum

proof

per cases ( 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 ) ) by A7, A8, A11;

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

now

per cases ( 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 ) ) by A7, A10, A11;

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

consider x being set such that
A14: x in P by A1, XBOOLE_0:def 1;
P c= dom T by TREES_1:def 14;
then reconsider x = x as Element of dom T by A14;
consider p' being FinSequence of NAT such that
A15: p' = x ;
D1 . q = T . q by A12, A14, A15;
hence contradiction by A11, A13, A14, A15; :: thesis: verum

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: contradiction

then consider p2, r2 being FinSequence of NAT such that
A16: ( p2 in P & r2 in dom T1 & q = p2 ^ r2 & D2 . q = T1 . r2 ) ;
not p2 is_a_prefix_of q by A12, A16;
hence contradiction by A16, TREES_1:8; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

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: contradiction

then consider p1, r1 being FinSequence of NAT such that
A17: ( p1 in P & r1 in dom T1 & q = p1 ^ r1 & D1 . q = T1 . r1 ) ;

now

per cases ( 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 ) ) 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: contradiction

then not p1 is_a_prefix_of q by A17;
hence contradiction by A17, TREES_1:8; :: thesis: verum

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: contradiction

then consider p2, r2 being FinSequence of NAT such that
A18: ( p2 in P & r2 in dom T1 & q = p2 ^ r2 & D2 . q = T1 . r2 ) ;

now

assume A19: p1 <> p2 ; :: thesis: contradiction
p1,p2 are_c=-comparable by A17, A18, Th1;
hence contradiction by A17, A18, A19, TREES_1:def 13; :: thesis: verum

end;

hence contradiction by A11, A17, A18, FINSEQ_1:46; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

end;

end;

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