let T1, T2 be DecoratedTree; :: thesis: ( dom T1 = dom T2 & ( for p being FinSequence of NAT st p in dom T1 holds
T1 . p = T2 . p ) implies T1 = T2 )
assume that
A1: dom T1 = dom T2 and
A2: for p being FinSequence of NAT st p in dom T1 holds
T1 . p = T2 . p ; :: thesis: T1 = T2

now :: thesis: for x being object st x in dom T1 holds
T1 . x = T2 . x

let x be object ; :: thesis: ( x in dom T1 implies T1 . x = T2 . x )
assume x in dom T1 ; :: thesis: T1 . x = T2 . x
then reconsider p = x as Element of dom T1 ;
T1 . p = T2 . p by A2;
hence T1 . x = T2 . x ; :: thesis: verum

end;

hence T1 = T2 by A1; :: thesis: verum