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
A22: 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
A23: for p being Node of T st ( not p in Leaves (dom T) or T . p <> x ) holds
T1 . p = T . p and
A24: 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
A25: 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
A26: for p being Node of T st ( not p in Leaves (dom T) or T . p <> x ) holds
T2 . p = T . p and
A27: 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
A28: 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 A22;
hence ( ( not p in dom T1 or p in dom T2 ) & ( not p in dom T2 or p in dom T1 ) ) by A25; :: thesis: verum

end;

reconsider p9 = {} as Node of T9 by TREES_1:22;

now :: thesis: for y being object st y in dom T1 holds
T1 . y = T2 . y

let y be object ; :: 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 A22;

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

then A30: T1 . (p ^ p9) = T9 . p9 by A24;
p ^ p9 = p by FINSEQ_1:34;
hence T1 . y = T2 . y by A27, A29, A30; :: thesis: verum

end;

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

then T1 . p = T . p by A23;
hence T1 . y = T2 . y by A26, A31; :: 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
A32: ( q in Leaves (dom T) & T . q = x & p = q ^ r ) ;
thus T1 . y = T9 . r by A24, A32
.= T2 . y by A27, A32 ; :: thesis: verum

end;

end;

end;

hence T1 = T2 by A28; :: thesis: verum