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
A13: dom D1 = tree (dom T),P,(dom T1) and
A14: 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
A15: dom D2 = tree (dom T),P,(dom T1) and
A16: 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 that
A18: q in dom D1 and
A19: 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 A13, A14, A18;

suppose A20: 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 A13, A16, A18;

suppose A22: 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
A23: 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 A23;
A25: ex p9 being FinSequence of NAT st p9 = x ;
then D1 . q = T . q by A20, A23;
hence contradiction by A19, A22, A23, A25; :: 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
A28: p2 in P and
r2 in dom T1 and
A29: q = p2 ^ r2 and
D2 . q = T1 . r2 ;
not p2 is_a_prefix_of q by A20, A28;
hence contradiction by A29, 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
A32: p1 in P and
r1 in dom T1 and
A33: q = p1 ^ r1 and
A34: 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 A13, A16, A18;

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 A32;
hence contradiction by A33, 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
A39: p2 in P and
r2 in dom T1 and
A40: q = p2 ^ r2 and
A41: D2 . q = T1 . r2 ;

now

assume A43: p1 <> p2 ; :: thesis: contradiction
p1,p2 are_c=-comparable by A33, A40, Th1;
hence contradiction by A32, A39, A43, TREES_1:def 13; :: thesis: verum

end;

hence contradiction by A19, A33, A34, A40, A41, FINSEQ_1:46; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

end;

end;

hence D1 = D2 by A13, A15, TREES_2:33; :: thesis: verum