let T1, T2 be DecoratedTree; :: thesis: ( ( for p being FinSequence holds
( p in dom T1 iff ( p in dom T or ex q being Node of T ex r being Node of T' st
( q in Leaves (dom T) & T . q = x & p = q ^ r ) ) ) ) & ( for p being Node of T st ( not p in Leaves (dom T) or T . p <> x ) holds
T1 . p = T . p ) & ( for p being Node of T
for q being Node of T' st p in Leaves (dom T) & T . p = x holds
T1 . (p ^ q) = T' . q ) & ( for p being FinSequence holds
( p in dom T2 iff ( p in dom T or ex q being Node of T ex r being Node of T' st
( q in Leaves (dom T) & T . q = x & p = q ^ r ) ) ) ) & ( for p being Node of T st ( not p in Leaves (dom T) or T . p <> x ) holds
T2 . p = T . p ) & ( for p being Node of T
for q being Node of T' st p in Leaves (dom T) & T . p = x holds
T2 . (p ^ q) = T' . q ) implies T1 = T2 )
assume that
A16: for p being FinSequence holds
( p in dom T1 iff ( p in dom T or ex q being Node of T ex r being Node of T' st
( q in Leaves (dom T) & T . q = x & p = q ^ r ) ) ) and
A17: for p being Node of T st ( not p in Leaves (dom T) or T . p <> x ) holds
T1 . p = T . p and
A18: for p being Node of T
for q being Node of T' st p in Leaves (dom T) & T . p = x holds
T1 . (p ^ q) = T' . q and
A19: for p being FinSequence holds
( p in dom T2 iff ( p in dom T or ex q being Node of T ex r being Node of T' st
( q in Leaves (dom T) & T . q = x & p = q ^ r ) ) ) and
A20: for p being Node of T st ( not p in Leaves (dom T) or T . p <> x ) holds
T2 . p = T . p and
A21: for p being Node of T
for q being Node of T' st p in Leaves (dom T) & T . p = x holds
T2 . (p ^ q) = T' . q ; :: thesis: T1 = T2
A22: dom T1 = dom T2

proof

let p be FinSequence of NAT ; :: according to TREES_2:def 1 :: thesis: ( ( not p in dom T1 or p in dom T2 ) & ( not p in dom T2 or p in dom T1 ) )
( ( not p in dom T1 or p in dom T or ex q being Node of T ex r being Node of T' st
( q in Leaves (dom T) & T . q = x & p = q ^ r ) ) & ( ( p in dom T or ex q being Node of T ex r being Node of T' st
( q in Leaves (dom T) & T . q = x & p = q ^ r ) ) implies p in dom T1 ) & ( not p in dom T2 or p in dom T or ex q being Node of T ex r being Node of T' st
( q in Leaves (dom T) & T . q = x & p = q ^ r ) ) & ( ( p in dom T or ex q being Node of T ex r being Node of T' st
( q in Leaves (dom T) & T . q = x & p = q ^ r ) ) implies p in dom T2 ) ) by A16, A19;
hence ( ( not p in dom T1 or p in dom T2 ) & ( not p in dom T2 or p in dom T1 ) ) ; :: thesis: verum

end;

reconsider p' = {} as Node of T' by TREES_1:47;

now

let y be set ; :: thesis: ( y in dom T1 implies T1 . b₁ = T2 . b₁ )
assume y in dom T1 ; :: thesis: T1 . b₁ = T2 . b₁
then reconsider p = y as Node of T1 ;

per cases ( p in dom T or ex q being Node of T ex r being Node of T' st
( q in Leaves (dom T) & T . q = x & p = q ^ r ) ) by A16;

suppose p in dom T ; :: thesis: T1 . b₁ = T2 . b₁

then reconsider p = p as Node of T ;

hereby :: thesis: verum

per cases ( ( p in Leaves (dom T) & T . p = x ) or not p in Leaves (dom T) or T . p <> x ) ;

suppose A23: ( p in Leaves (dom T) & T . p = x ) ; :: thesis: T1 . y = T2 . y

then ( T1 . (p ^ p') = T' . p' & p ^ p' = p ) by A18, FINSEQ_1:47;
hence T1 . y = T2 . y by A21, A23; :: thesis: verum

end;

suppose A24: ( not p in Leaves (dom T) or T . p <> x ) ; :: thesis: T1 . y = T2 . y

then T1 . p = T . p by A17;
hence T1 . y = T2 . y by A20, A24; :: thesis: verum

end;

end;

end;

end;

suppose ex q being Node of T ex r being Node of T' st
( q in Leaves (dom T) & T . q = x & p = q ^ r ) ; :: thesis: T1 . b₁ = T2 . b₁

then consider q being Node of T, r being Node of T' such that
A25: ( q in Leaves (dom T) & T . q = x & p = q ^ r ) ;
thus T1 . y = T' . r by A18, A25
.= T2 . y by A21, A25 ; :: thesis: verum

end;

end;

end;

hence T1 = T2 by A22, FUNCT_1:9; :: thesis: verum