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

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

hence
T1 = T2
by A7, A10; :: thesis: verumT1 . 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;

end;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 )

hence
T1 . x = T2 . x
by A8, A11, A13; :: thesis: verum( 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;thus T1 . x = p . (n + 1) by A9, A14

.= T2 . x by A12, A14 ; :: thesis: verum