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 :: thesis: for q being FinSequence of NAT st q in dom D1 holds
not D1 . q <> D2 . q
let q be FinSequence of NAT ; :: thesis: ( q in dom D1 implies not D1 . q <> D2 . q )
assume that
A11: q in dom D1 and
A12: 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 A13: 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 :: thesis: contradiction
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 A14: 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 object such that
A15: x in P by ;
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 ;
hence contradiction by A12, A14, A15, A16; :: 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
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 ;
hence contradiction by A18, TREES_1:1; :: 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
A19: p1 in P and
r1 in dom T1 and
A20: q = p1 ^ r1 and
A21: D1 . q = T1 . r1 ;
now :: thesis: contradiction
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
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
A22: p2 in P and
r2 in dom T1 and
A23: q = p2 ^ r2 and
A24: D2 . q = T1 . r2 ;
hence contradiction by A12, A20, A21, A23, A24, FINSEQ_1:33; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
end;
end;
end;
hence D1 = D2 by ; :: thesis: verum