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

( 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

reconsider p9 = {} as Node of T9 by TREES_1:22;
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;( 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

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

T1 . y = T2 . y

hence
T1 = T2
by A28; :: thesis: verumT1 . y = T2 . y

let y be object ; :: thesis: ( y in dom T1 implies T1 . b_{1} = T2 . b_{1} )

assume y in dom T1 ; :: thesis: T1 . b_{1} = T2 . b_{1}

then reconsider p = y as Node of T1 ;

end;assume y in dom T1 ; :: thesis: T1 . 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;

end;

( q in Leaves (dom T) & T . q = x & p = q ^ r ) ) by A22;

suppose
p in dom T
; :: thesis: T1 . b_{1} = T2 . b_{1}

then reconsider p = p as Node of T ;

end;hereby :: thesis: verum
end;

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

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_{1} = T2 . b_{1}

( q in Leaves (dom T) & T . q = x & p = q ^ r ) ; :: thesis: T1 . 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;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