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) and
A14: T1 . {} = x and
A15: for n being Element of NAT st n < len p holds
T1 . <*n*> = p . (n + 1) and
A16: dom T2 = elementary_tree (len p) and
A17: T2 . {} = x and
A18: for n being Element of NAT st n < len p holds
T2 . <*n*> = p . (n + 1) ; :: thesis: T1 = T2

A19: now

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

A22: now

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

end;

thus T1 . x = T2 . x by A14, A17, A21, A22; :: thesis: verum

end;

thus T1 = T2 by A13, A16, A19, FUNCT_1:9; :: thesis: verum