let T1, T2 be DecoratedTree; :: thesis: ( dom T1 = elementary_tree (len p) & T1 . {} = x & ( for n being Element of NAT st n < len p holds
T1 . <*n*> = p . (n + 1) ) & dom T2 = elementary_tree (len p) & T2 . {} = x & ( for n being Element of NAT st n < len p holds
T2 . <*n*> = p . (n + 1) ) implies T1 = T2 )
assume that
A13: ( dom T1 = elementary_tree (len p) & T1 . {} = x & ( for n being Element of NAT st n < len p holds
T1 . <*n*> = p . (n + 1) ) ) and
A14: ( dom T2 = elementary_tree (len p) & T2 . {} = x & ( for n being Element of NAT st n < len p holds
T2 . <*n*> = p . (n + 1) ) ) ; :: thesis: T1 = T2

now

let x be set ; :: thesis: ( x in elementary_tree (len p) implies T1 . x = T2 . x )
assume x in elementary_tree (len p) ; :: thesis: T1 . x = T2 . x
then reconsider x' = x as Element of elementary_tree (len p) ;
A15: ( x' = {} or ex n being Element of NAT st
( n < len p & x' = <*n*> ) ) by TREES_1:57;

now

given n being Element of NAT such that A16: ( n < len p & x = <*n*> ) ; :: thesis: T1 . x = T2 . x
thus T1 . x = p . (n + 1) by A13, A16
.= T2 . x by A14, A16 ; :: thesis: verum

end;

hence T1 . x = T2 . x by A13, A14, A15; :: thesis: verum

end;

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