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 T9 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 T9 st p in Leaves (dom T) & T . p = x holds
T1 . (p ^ q) = T9 . 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 T9 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 T9 st p in Leaves (dom T) & T . p = x holds
T2 . (p ^ q) = T9 . q ) implies T1 = T2 )
assume that
A40: 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 T9 st
( q in Leaves (dom T) & T . q = x & p = q ^ r ) ) ) and
A41: for p being Node of T st ( not p in Leaves (dom T) or T . p <> x ) holds
T1 . p = T . p and
A42: for p being Node of T
for q being Node of T9 st p in Leaves (dom T) & T . p = x holds
T1 . (p ^ q) = T9 . q and
A43: 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 T9 st
( q in Leaves (dom T) & T . q = x & p = q ^ r ) ) ) and
A44: for p being Node of T st ( not p in Leaves (dom T) or T . p <> x ) holds
T2 . p = T . p and
A45: for p being Node of T
for q being Node of T9 st p in Leaves (dom T) & T . p = x holds
T2 . (p ^ q) = T9 . q ; :: thesis: T1 = T2
A46: 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 ) )
( p in dom T1 iff ( p in dom T or ex q being Node of T ex r being Node of T9 st
( q in Leaves (dom T) & T . q = x & p = q ^ r ) ) ) by A40;
hence ( ( not p in dom T1 or p in dom T2 ) & ( not p in dom T2 or p in dom T1 ) ) by A43; :: thesis: verum

end;

reconsider p9 = {} as Node of T9 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 T9 st
( q in Leaves (dom T) & T . q = x & p = q ^ r ) ) by A40;

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 A51: ( p in Leaves (dom T) & T . p = x ) ; :: thesis: T1 . y = T2 . y

then A52: T1 . (p ^ p9) = T9 . p9 by A42;
p ^ p9 = p by FINSEQ_1:47;
hence T1 . y = T2 . y by A45, A51, A52; :: thesis: verum

end;

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

then T1 . p = T . p by A41;
hence T1 . y = T2 . y by A44, A54; :: thesis: verum

end;

end;

end;

end;

suppose ex q being Node of T ex r being Node of T9 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 T9 such that
A57: ( q in Leaves (dom T) & T . q = x & p = q ^ r ) ;
thus T1 . y = T9 . r by A42, A57
.= T2 . y by A45, A57 ; :: thesis: verum

end;

end;

end;

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