let T1, T2 be DecoratedTree; :: thesis: ( dom T1 = elementary_tree (len p) & T1 . {} = x & ( for n being Nat st n < len p holds
T1 . <*n*> = p . (n + 1) ) & dom T2 = elementary_tree (len p) & T2 . {} = x & ( for n being Nat st n < len p holds
T2 . <*n*> = p . (n + 1) ) implies T1 = T2 )
assume that
A7: dom T1 = elementary_tree (len p) and
A8: T1 . {} = x and
A9: for n being Nat st n < len p holds
T1 . <*n*> = p . (n + 1) and
A10: dom T2 = elementary_tree (len p) and
A11: T2 . {} = x and
A12: for n being Nat st n < len p holds
T2 . <*n*> = p . (n + 1) ; :: thesis: T1 = T2

now :: thesis: for x being object st x in elementary_tree (len p) holds
T1 . x = T2 . x

let x be object ; :: 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 x9 = x as Element of elementary_tree (len p) ;
A13: ( x9 = {} or ex n being Nat st
( n < len p & x9 = <*n*> ) ) by TREES_1:30;

now :: thesis: ( ex n being Nat st
( n < len p & x = <*n*> ) implies T1 . x = T2 . x )

given n being Nat such that A14: ( n < len p & x = <*n*> ) ; :: thesis: T1 . x = T2 . x
thus T1 . x = p . (n + 1) by A9, A14
.= T2 . x by A12, A14 ; :: thesis: verum

end;

hence T1 . x = T2 . x by A8, A11, A13; :: thesis: verum

end;

hence T1 = T2 by A7, A10; :: thesis: verum